From bb338842d31bcae3a3e5aa2136126ae676dbd21c Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Thu, 6 Feb 2020 09:10:58 +0100 Subject: [PATCH 1/7] Moving to coq 8.10 --- .gitignore | 4 + Makefile | 34 ++--- coqine.opam | 16 +++ dune-project | 3 + encodings/theories/f_matita.dk | 1 + encodings/theories/fpredicates.dk | 1 + encodings/theories/functional.dk | 1 + encodings/theories/lift-predicates.dk | 1 + encodings/theories/original.dk | 1 + encodings/theories/predicates.dk | 1 + encodings/theories/predicates_ac.dk | 1 + run/main/Makefile | 7 +- run/main/Test/Debug.v | 9 +- run/main/import_debug.v | 11 +- run/main/main_debug.v | 2 +- src/cname.ml | 27 +++- src/cname.mli | 21 ++- src/commands.ml4 | 101 -------------- src/commands.mlg | 50 +++---- src/debug.ml | 47 ++++--- src/debug.mli | 11 +- src/dune | 25 ++++ src/encoding.ml | 78 +++++------ src/inductives.ml | 132 ++++++++++++------ src/info.ml | 3 +- src/libraries.ml | 62 +++------ src/libraries.mli | 16 +-- src/modules.ml | 16 ++- src/terms.ml | 190 +++++++++++++------------- src/terms.mli | 20 ++- src/translator.ml | 3 + src/translator.mli | 9 +- src/tsorts.ml | 15 +- src/tsorts.mli | 3 +- src/tunivs.ml | 26 ++-- 35 files changed, 509 insertions(+), 439 deletions(-) create mode 100644 coqine.opam create mode 100644 dune-project delete mode 100644 src/commands.ml4 create mode 100644 src/dune diff --git a/.gitignore b/.gitignore index 4aec235..2e207fc 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,10 @@ *.dko *.tar.bz2 +# dune files. +_build/ + + summary.csv run/main/**/*.dk diff --git a/Makefile b/Makefile index 8beb418..2eb76a4 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,6 @@ +# Compile with "make Q=" to display the commands that are run. +Q = @ + # Variables COQ_MAKEFILE ?= coq_makefile COQTOP ?= coqtop @@ -10,7 +13,7 @@ CAMLFLAGS="-bin-annot -annot" RUNDIR=run COQ_VERSION := $(shell $(COQTOP) -print-version) -CHECK_VERSION := $(shell $(COQTOP) -print-version | grep "8\.8\.*") +CHECK_VERSION := $(shell $(COQTOP) -print-version | grep "8\.10\.*") define MANUAL @@ -95,25 +98,25 @@ check-version: ifeq ("$(CHECK_VERSION)","") $(warning "Incorrect Coq version !") $(warning "Found: $(COQ_VERSION).") - $(warning "Expected: 8.8.x") + $(warning "Expected: 8.1°.x") $(error "To ignore this, use: make CHECK_VERSION=ignore") endif -plugin: CoqMakefile - make -f CoqMakefile VERBOSE=$(VERBOSE) - all +plugin: + $(Q)dune build -install: CoqMakefile plugin - make -f CoqMakefile - install +doc: + $(Q)dune build @doc -uninstall: CoqMakefile - make -f CoqMakefile - uninstall +install: all + $(Q)dune install -.merlin: CoqMakefile - make -f CoqMakefile .merlin +uninstall: all + $(Q)dune uninstall -clean: CoqMakefile +clean: + $(Q)dune clean make -C encodings - clean - make -f CoqMakefile - clean make -C $(RUNDIR)/main clean make -C $(RUNDIR)/mathcomp clean @@ -129,7 +132,6 @@ clean: CoqMakefile rm -f $(RUNDIR)/mathcomp/config.v rm -f $(RUNDIR)/logipedia/config.v rm -f $(RUNDIR)/upoly_logipedia/config.v - rm -f CoqMakefile rm -f *.tar.bz2 rm -f summary.csv @@ -138,9 +140,9 @@ fullclean: clean rm src/*.cmti rm src/*.annot -CoqMakefile: Make - $(COQ_MAKEFILE) -f Make -o CoqMakefile - echo "COQMF_CAMLFLAGS+=-annot -bin-annot -g" >> CoqMakefile.conf +# CoqMakefile: Make +# $(COQ_MAKEFILE) -f Make -o CoqMakefile +# echo "COQMF_CAMLFLAGS+=-annot -bin-annot -g" >> CoqMakefile.conf .coqrc: plugin echo "Add ML Path \"$(shell pwd)/src\"." > .coqrc diff --git a/coqine.opam b/coqine.opam new file mode 100644 index 0000000..349c52d --- /dev/null +++ b/coqine.opam @@ -0,0 +1,16 @@ +synopsis: "Coqine Plugin" +description: "Coqine Plugin" +name: "coqine" +opam-version: "2.0" +maintainer: "gaspard.ferey@mines.org" +authors: "Gaspard FEREY" +homepage: "https://github.com/Deducteam/CoqInE/" +bug-reports: "https://github.com/Deducteam/CoqInE/" +dev-repo: "git+https://github.com/Deducteam/CoqInE" +license: "GPL 3" +depends: [ + "ocaml" { >= "4.04.0" } + "coq" { = "8.8.2" } + "dune" { build & >= "1.9.0" } +] +build: [ "dune" "build" "-p" name "-j" jobs ] diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..3adadc2 --- /dev/null +++ b/dune-project @@ -0,0 +1,3 @@ +(lang dune 1.9) +(using coq 0.1) +(name coqine) diff --git a/encodings/theories/f_matita.dk b/encodings/theories/f_matita.dk index e0995c9..4cb2002 100644 --- a/encodings/theories/f_matita.dk +++ b/encodings/theories/f_matita.dk @@ -22,6 +22,7 @@ def max : Nat -> Nat -> Nat. [i,j] max (s i) (s j) --> s (max i j). (; +Coqine sprop = prop Coqine prop = prop Coqine type = type Coqine set = set diff --git a/encodings/theories/fpredicates.dk b/encodings/theories/fpredicates.dk index ef241a7..2d94caa 100644 --- a/encodings/theories/fpredicates.dk +++ b/encodings/theories/fpredicates.dk @@ -25,6 +25,7 @@ def max : Nat -> Nat -> Nat. [i,j] max (s i) (s j) --> s (max i j). (; +Coqine sprop = prop Coqine prop = prop Coqine type = type Coqine set = set diff --git a/encodings/theories/functional.dk b/encodings/theories/functional.dk index 091aae3..e7dac66 100644 --- a/encodings/theories/functional.dk +++ b/encodings/theories/functional.dk @@ -23,6 +23,7 @@ def set : Sort := type z. def type0 : Sort := type (s z). (; +Coqine sprop = prop Coqine prop = prop Coqine type = type Coqine set = set diff --git a/encodings/theories/lift-predicates.dk b/encodings/theories/lift-predicates.dk index ea90631..f7be486 100644 --- a/encodings/theories/lift-predicates.dk +++ b/encodings/theories/lift-predicates.dk @@ -22,6 +22,7 @@ def max : Nat -> Nat -> Nat. [i,j] max (s i) (s j) --> s (max i j). (; +Coqine sprop = prop Coqine prop = prop Coqine type = type Coqine set = set diff --git a/encodings/theories/original.dk b/encodings/theories/original.dk index 3a5217d..e80df34 100644 --- a/encodings/theories/original.dk +++ b/encodings/theories/original.dk @@ -23,6 +23,7 @@ set : Sort. type : Nat -> Sort. (; +Coqine sprop = prop Coqine prop = prop Coqine set = set Coqine type = type diff --git a/encodings/theories/predicates.dk b/encodings/theories/predicates.dk index bfae364..7a67607 100644 --- a/encodings/theories/predicates.dk +++ b/encodings/theories/predicates.dk @@ -25,6 +25,7 @@ def max : Nat -> Nat -> Nat. [i,j] max (s i) (s j) --> s (max i j). (; +Coqine sprop = prop Coqine prop = prop Coqine type = type Coqine set = set diff --git a/encodings/theories/predicates_ac.dk b/encodings/theories/predicates_ac.dk index d9bfb1e..270ee0a 100644 --- a/encodings/theories/predicates_ac.dk +++ b/encodings/theories/predicates_ac.dk @@ -24,6 +24,7 @@ def set : Sort := type z. def type0 : Sort := type (s z). (; +Coqine sprop = prop Coqine prop = prop Coqine type = type Coqine set = set diff --git a/run/main/Makefile b/run/main/Makefile index fe59eab..f35d797 100644 --- a/run/main/Makefile +++ b/run/main/Makefile @@ -2,14 +2,15 @@ # Variables COQ_MAKEFILE ?= coq_makefile -COQC ?= coqc +COQC ?= coqc -allow-sprop DKCHECK ?= dkcheck DKDEP ?= dkdep VERBOSE ?= MAINFILE ?= main_debug OUTFOLDER = out -COQINEPATH=../../src +COQINE_SRC=../../src/ +COQINE_LIB=../../_build/install/default/lib/coqine/plugin/ DKS = $(wildcard $(OUTFOLDER)/*.dk) DKOS = $(DKS:.dk=.dko) @@ -33,7 +34,7 @@ $(OUTFOLDER): # Generate the [.dk] files by executing [main_???.v] generate: compile $(OUTFOLDER) - $(COQC) -nois -init-file ../../.coqrc -verbose -R . Top $(MAINFILE).v + $(COQC) -nois -verbose -R . Top -Q $(COQINE_SRC) Coqine -I $(COQINE_LIB) $(MAINFILE).v # Generate the dependencies of [.dk] files depend: diff --git a/run/main/Test/Debug.v b/run/main/Test/Debug.v index 8bec527..4430b79 100644 --- a/run/main/Test/Debug.v +++ b/run/main/Test/Debug.v @@ -198,7 +198,8 @@ Section Defs. (** Any [Equivalence] declared in the context is automatically considered a rewrite crelation. *) - Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA. + Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA. + Defined. (** Leibniz equality. *) Section Leibniz. @@ -216,8 +217,8 @@ Section Defs. End Defs. (** Default rewrite crelations handled by [setoid_rewrite]. *) -Instance: RewriteRelation impl. -Instance: RewriteRelation iff. +Instance: RewriteRelation impl. Defined. +Instance: RewriteRelation iff. Defined. (** Hints to drive the typeclass resolution avoiding loops due to the use of full unification. *) @@ -320,7 +321,7 @@ Section Binary. Definition relation_equivalence : crelation (crelation A) := fun R R' => forall x y, iffT (R x y) (R' x y). - Global Instance: RewriteRelation relation_equivalence. + Global Instance: RewriteRelation relation_equivalence. Defined. Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A := fun x y => prod (R x y) (R' x y). diff --git a/run/main/import_debug.v b/run/main/import_debug.v index 22d39a5..8cb1e50 100644 --- a/run/main/import_debug.v +++ b/run/main/import_debug.v @@ -29,10 +29,11 @@ Fixpoint A m := fix A_m n := Definition t'' := A 2 2. +Set Allow StrictProp. + Require Import Test.Test Test.Identity - Coq.Classes.RelationClasses Test.Polymorph Test.ImportA Test.ImportB @@ -46,11 +47,17 @@ Require Import Test.Functors Test.NestedLibraries Test.Reflexivity +(* + Test.Debuglib +*) +. + +Require Import + Coq.Classes.RelationClasses (* Coq.Arith.PeanoNat - Test.Debuglib Coq.Logic.Berardi Coq.Logic.ChoiceFacts diff --git a/run/main/main_debug.v b/run/main/main_debug.v index 53eced5..b8c121e 100644 --- a/run/main/main_debug.v +++ b/run/main/main_debug.v @@ -10,7 +10,7 @@ Dedukti Set Destination "out". Dedukti Enable Debug. Dedukti Set Debug "debug.out". -Dedukti Add Debug "Coq.Init.Datatype". +Dedukti Add Debug "Coq.Init.Logic". Require Import import_debug. diff --git a/src/cname.ml b/src/cname.ml index 4416135..892d53e 100644 --- a/src/cname.ml +++ b/src/cname.ml @@ -14,6 +14,8 @@ open Info - inductive: refers to an inductive type - constructor: refers to a constructor of an inductive type *) +let mk_binder name = Context.make_annot name Sorts.Relevant + (** Fresh names *) let full_path info identifier = @@ -25,8 +27,8 @@ let push_global info identifier = (** Push a dummy declaration to declare an identifier locally. *) let push_identifier identifier env = - Environ.push_named - (Context.Named.Declaration.of_tuple (identifier, None, Constr.mkSort (Term.Prop(Term.Null)))) env + let dummy = Context.Named.Declaration.of_tuple (mk_binder identifier,None,Constr.mkProp) in + Environ.push_named dummy env (** Generate a fresh identifier that is different from any constant, inductive type, or constructor in the current module, and from any identifier in @@ -52,6 +54,9 @@ let fresh_of_name info env ?(global=false) ?prefix ~default name = | Names.Anonymous -> fresh_identifier info env ~global ?prefix (Names.Id.of_string default) | Names.Name(identifier) -> fresh_identifier info env ~global ?prefix identifier +let fresh_of_name_binder info env ?global:(global=false) ?prefix ~default name = + fresh_of_name info env ~global ?prefix ~default (Context.binder_name name) + let fresh_name info env ?prefix ?default name = match name, default with | Names.Name(identifier), _ -> Names.Name (fresh_identifier info env ?prefix identifier) @@ -59,6 +64,17 @@ let fresh_name info env ?prefix ?default name = | Names.Anonymous, Some(d) -> Names.Name (fresh_of_string info env ?prefix d) +let fresh info env ?prefix ?default binder = + let name = Context.binder_name binder in + let fresh_name = fresh_name ?prefix ?default info env name in + let fresh_binder = Context.make_annot fresh_name Sorts.Relevant in + fresh_name, fresh_binder + +let fresh_binder info env ?prefix ?default binder = + let name = Context.binder_name binder in + let fresh_name = fresh_name info env name in + Context.make_annot fresh_name Sorts.Relevant + (** Name of the match function for the inductive type *) let constraint_name index = "cstr_" ^ (string_of_int index) @@ -100,10 +116,11 @@ let escape name = let translate_identifier identifier = escape (Names.Id.to_string identifier) -let translate_name ?(ensure_name = false) name = - match name with +let translate_name = function | Names.Name(identifier) -> translate_identifier identifier - | Names.Anonymous -> if ensure_name then failwith "Anonymous name" else "" + | Names.Anonymous -> failwith "Anonymous name" + +let translate_binder b = translate_name (Context.binder_name b) let translate_dir_path dir_path = escape (Names.DirPath.to_string dir_path) diff --git a/src/cname.mli b/src/cname.mli index 78537bf..c6cfa3f 100644 --- a/src/cname.mli +++ b/src/cname.mli @@ -1,5 +1,7 @@ (** Translation of Coq names *) +val mk_binder : 'a -> 'a Context.binder_annot + val full_path : Info.info -> Names.Id.t -> Libnames.full_path val push_global : Info.info -> Names.variable -> unit @@ -19,10 +21,25 @@ val fresh_of_name : Info.info -> Environ.env -> ?global:bool -> ?prefix:string -> default:string -> Names.Name.t -> Names.Id.t +val fresh_of_name_binder : + Info.info -> Environ.env -> + ?global:bool -> ?prefix:string -> default:string -> + Names.Name.t Context.binder_annot -> Names.Id.t + val fresh_name : Info.info -> Environ.env -> ?prefix:string -> ?default:string -> Names.Name.t -> Names.Name.t +val fresh_binder : + Info.info -> Environ.env -> + ?prefix:string -> ?default:string -> Names.Name.t Context.binder_annot -> + Names.Name.t Context.binder_annot + +val fresh : + Info.info -> Environ.env -> + ?prefix:string -> ?default:string -> Names.Name.t Context.binder_annot -> + Names.Name.t * Names.Name.t Context.binder_annot + val constraint_name : int -> string @@ -37,7 +54,9 @@ val escape : string -> string val translate_identifier : Names.Id.t -> string -val translate_name : ?ensure_name:bool -> Names.Name.t -> string +val translate_name : Names.Name.t -> string + +val translate_binder : Names.Name.t Context.binder_annot -> string val translate_dir_path : Names.DirPath.t -> string diff --git a/src/commands.ml4 b/src/commands.ml4 deleted file mode 100644 index 641869c..0000000 --- a/src/commands.ml4 +++ /dev/null @@ -1,101 +0,0 @@ -(*i camlp4deps: "grammar/grammar.cma" i*) - -DECLARE PLUGIN "coqine_plugin" - -open Libraries -open Modules -open Stdarg - - -(** Exporting to Dedukti **) - -VERNAC COMMAND EXTEND DeduktiExportLibrary CLASSIFIED AS QUERY -| [ "Dedukti" "Export" "Library" global_list(refs) ] -> - [ List.iter translate_library refs ] -END - -VERNAC COMMAND EXTEND DeduktiExportUniverses CLASSIFIED AS QUERY -| [ "Dedukti" "Export" "Universes" ] -> - [ translate_universes () ] -END - -VERNAC COMMAND EXTEND DeduktiExportAll CLASSIFIED AS QUERY -| [ "Dedukti" "Export" "All" ] -> - [ translate_all () ] -END - -VERNAC COMMAND EXTEND DeduktiExportAllBut CLASSIFIED AS QUERY -| [ "Dedukti" "Export" "All" "But" global_list(refs) ] -> - [ translate_all_but refs ] -END - - -(** Printing universes **) - -VERNAC COMMAND EXTEND DeduktiShowUniverses CLASSIFIED AS QUERY -| [ "Dedukti" "Show" "Universes" ] -> - [ show_universes_constraints () ] -END - -VERNAC COMMAND EXTEND DeduktiShowSortedUniverses CLASSIFIED AS QUERY -| [ "Dedukti" "Show" "Sorted" "Universes" ] -> - [ show_sorted_universes_constraints () ] -END - - -(** Setting parameters **) - -VERNAC COMMAND EXTEND EnableFailProofMode CLASSIFIED AS QUERY -| [ "Dedukti" "Enable" "Failproofmode" ] -> - [ enable_failproofmode () ] -END - -VERNAC COMMAND EXTEND DisableFailProofMode CLASSIFIED AS QUERY -| [ "Dedukti" "Disable" "Failproofmode" ] -> - [ disable_failproofmode () ] -END - -VERNAC COMMAND EXTEND DeduktiSetDestination CLASSIFIED AS QUERY -| [ "Dedukti" "Set" "Destination" string(dest) ] -> - [ Info.set_destination dest ] -END - -VERNAC COMMAND EXTEND DeduktiSetDebug CLASSIFIED AS QUERY -| [ "Dedukti" "Set" "Debug" string(dest) ] -> - [ Debug.debug_to_file dest ] -END - -VERNAC COMMAND EXTEND DeduktiAddDebug CLASSIFIED AS QUERY -| [ "Dedukti" "Add" "Debug" string(lib) ] -> - [ Debug.add_debug_lib lib ] -END - -VERNAC COMMAND EXTEND DeduktiFilterSymb CLASSIFIED AS QUERY -| [ "Dedukti" "Filter" "Out" string(symb) ] -> - [ Modules.filter_out symb ] -END - -VERNAC COMMAND EXTEND DeduktiEnableVerbose CLASSIFIED AS QUERY -| [ "Dedukti" "Enable" "Verbose" ] -> - [ Debug.enable_verbose () ] -END - -VERNAC COMMAND EXTEND DeduktiDisableVerbose CLASSIFIED AS QUERY -| [ "Dedukti" "Disable" "Verbose" ] -> - [ Debug.disable_verbose () ] -END - -VERNAC COMMAND EXTEND DeduktiEnableDebug CLASSIFIED AS QUERY -| [ "Dedukti" "Enable" "Debug" ] -> - [ Debug.enable_debug () ] -END - -VERNAC COMMAND EXTEND DeduktiDisableDebug CLASSIFIED AS QUERY -| [ "Dedukti" "Disable" "Debug" ] -> - [ Debug.disable_debug () ] -END - -VERNAC COMMAND EXTEND DeduktiSetParam CLASSIFIED AS QUERY -| [ "Dedukti" "Set" "Param" string(key) string(value) ] -> - [ Encoding.set_param key value ] -END diff --git a/src/commands.mlg b/src/commands.mlg index 66a9d6f..52cc6d2 100644 --- a/src/commands.mlg +++ b/src/commands.mlg @@ -10,93 +10,87 @@ open Stdarg (** Exporting to Dedukti **) +(* +VERNAC COMMAND EXTEND DeduktiTranslateTerm CLASSIFIED AS QUERY +| [ "Dedukti" "Translate" constr(t) ] -> + { translate_term t } +END +*) + VERNAC COMMAND EXTEND DeduktiExportLibrary CLASSIFIED AS QUERY - [ "Dedukti" "Export" "Library" global_list(refs) ] -> +| [ "Dedukti" "Export" "Library" global_list(refs) ] -> { List.iter translate_library refs } END VERNAC COMMAND EXTEND DeduktiExportUniverses CLASSIFIED AS QUERY - [ "Dedukti" "Export" "Universes" ] -> +| [ "Dedukti" "Export" "Universes" ] -> { translate_universes () } END VERNAC COMMAND EXTEND DeduktiExportAll CLASSIFIED AS QUERY - [ "Dedukti" "Export" "All" ] -> +| [ "Dedukti" "Export" "All" ] -> { translate_all () } END VERNAC COMMAND EXTEND DeduktiExportAllBut CLASSIFIED AS QUERY - [ "Dedukti" "Export" "All" "But" global_list(refs) ] -> +| [ "Dedukti" "Export" "All" "But" global_list(refs) ] -> { translate_all_but refs } END -(** Printing universes **) - -VERNAC COMMAND EXTEND DeduktiShowUniverses CLASSIFIED AS QUERY - [ "Dedukti" "Show" "Universes" ] -> - { show_universes_constraints () } -END - -VERNAC COMMAND EXTEND DeduktiShowSortedUniverses CLASSIFIED AS QUERY - [ "Dedukti" "Show" "Sorted" "Universes" ] -> - { show_sorted_universes_constraints () } -END - - (** Setting parameters **) VERNAC COMMAND EXTEND EnableFailProofMode CLASSIFIED AS QUERY - [ "Dedukti" "Enable" "Failproofmode" ] -> +| [ "Dedukti" "Enable" "Failproofmode" ] -> { enable_failproofmode () } END VERNAC COMMAND EXTEND DisableFailProofMode CLASSIFIED AS QUERY - [ "Dedukti" "Disable" "Failproofmode" ] -> +| [ "Dedukti" "Disable" "Failproofmode" ] -> { disable_failproofmode () } END VERNAC COMMAND EXTEND DeduktiSetDestination CLASSIFIED AS QUERY - [ "Dedukti" "Set" "Destination" string(dest) ] -> +| [ "Dedukti" "Set" "Destination" string(dest) ] -> { Info.set_destination dest } END VERNAC COMMAND EXTEND DeduktiSetDebug CLASSIFIED AS QUERY - [ "Dedukti" "Set" "Debug" string(dest) ] -> +| [ "Dedukti" "Set" "Debug" string(dest) ] -> { Debug.debug_to_file dest } END VERNAC COMMAND EXTEND DeduktiAddDebug CLASSIFIED AS QUERY - [ "Dedukti" "Add" "Debug" string(lib) ] -> +| [ "Dedukti" "Add" "Debug" string(lib) ] -> { Debug.add_debug_lib lib } END VERNAC COMMAND EXTEND DeduktiFilterSymb CLASSIFIED AS QUERY - [ "Dedukti" "Filter" "Out" string(symb) ] -> +| [ "Dedukti" "Filter" "Out" string(symb) ] -> { Modules.filter_out symb } END VERNAC COMMAND EXTEND DeduktiEnableVerbose CLASSIFIED AS QUERY - [ "Dedukti" "Enable" "Verbose" ] -> +| [ "Dedukti" "Enable" "Verbose" ] -> { Debug.enable_verbose () } END VERNAC COMMAND EXTEND DeduktiDisableVerbose CLASSIFIED AS QUERY - [ "Dedukti" "Disable" "Verbose" ] -> +| [ "Dedukti" "Disable" "Verbose" ] -> { Debug.disable_verbose () } END VERNAC COMMAND EXTEND DeduktiEnableDebug CLASSIFIED AS QUERY - [ "Dedukti" "Enable" "Debug" ] -> +| [ "Dedukti" "Enable" "Debug" ] -> { Debug.enable_debug () } END VERNAC COMMAND EXTEND DeduktiDisableDebug CLASSIFIED AS QUERY - [ "Dedukti" "Disable" "Debug" ] -> +| [ "Dedukti" "Disable" "Debug" ] -> { Debug.disable_debug () } END VERNAC COMMAND EXTEND DeduktiSetParam CLASSIFIED AS QUERY - [ "Dedukti" "Set" "Param" string(key) string(value) ] -> +| [ "Dedukti" "Set" "Param" string(key) string(value) ] -> { Encoding.set_param key value } END diff --git a/src/debug.ml b/src/debug.ml index dcd5123..585e207 100644 --- a/src/debug.ml +++ b/src/debug.ml @@ -68,10 +68,12 @@ let pp_coq_term_env env = printer_of_std_ppcmds (Printer.safe_pr_constr_env env (Evd.from_env env)) let pp_coq_term = - let (sigma, env) = Pfedit.get_current_context () in + let env = Global.env () in + let sigma = Evd.from_env env in printer_of_std_ppcmds (Printer.safe_pr_constr_env env sigma) let pp_coq_type = - let (sigma, env) = Pfedit.get_current_context () in + let env = Global.env () in + let sigma = Evd.from_env env in printer_of_std_ppcmds (Printer.pr_type_env env sigma) let pp_coq_level = printer_of_std_ppcmds Univ.Level.pr let pp_coq_univ = printer_of_std_ppcmds Univ.Universe.pr @@ -89,26 +91,39 @@ let pp_coq_name fmt = function | Names.Name.Anonymous -> fprintf fmt "_" | Names.Name.Name n -> fprintf fmt "%a" pp_coq_id n +let pp_coq_binder pp fmt binder = pp fmt (Context.binder_name binder) + let pp_coq_kername = printer_of_std_ppcmds Names.KerName.print let pp_coq_sort fmt = function - | Term.Prop Term.Null -> fprintf fmt "Set" - | Term.Prop Term.Pos -> fprintf fmt "Prop" - | Term.Type i -> fprintf fmt "Univ(%a)" pp_coq_univ i + | Term.SProp -> fprintf fmt "SProp" + | Term.Set -> fprintf fmt "Set" + | Term.Prop -> fprintf fmt "Prop" + | Term.Type i -> fprintf fmt "Univ(%a)" pp_coq_univ i let pp_coq_decl fmt = function - | Context.Rel.Declaration.LocalAssum (name, t) -> - fprintf fmt "%a : %a" pp_coq_name name pp_coq_term t - | Context.Rel.Declaration.LocalDef (name, v, t) -> - fprintf fmt "%a : %a = %a" pp_coq_name name pp_coq_term t pp_coq_term t + | Context.Rel.Declaration.LocalAssum (binder, t) -> + fprintf fmt "%a : %a" + (pp_coq_binder pp_coq_name) binder + pp_coq_term t + | Context.Rel.Declaration.LocalDef (binder, v, t) -> + fprintf fmt "%a : %a = %a" + (pp_coq_binder pp_coq_name) binder + pp_coq_term v + pp_coq_term t let pp_coq_arity_ctxt fmt = pp_list " -> " pp_coq_decl fmt let pp_coq_named_decl fmt = function - | Context.Named.Declaration.LocalAssum (id, t) -> - fprintf fmt "%a = %a" pp_coq_id id pp_coq_term t - | Context.Named.Declaration.LocalDef (id, v, t) -> - fprintf fmt "%a : %a = %a" pp_coq_id id pp_coq_term t pp_coq_term t + | Context.Named.Declaration.LocalAssum (binder, t) -> + fprintf fmt "%a = %a" + (pp_coq_binder pp_coq_id) binder + pp_coq_term t + | Context.Named.Declaration.LocalDef (binder, v, t) -> + fprintf fmt "%a : %a = %a" + (pp_coq_binder pp_coq_id) binder + pp_coq_term v + pp_coq_term t let pp_coq_ctxt fmt ctxt = fprintf fmt "[\n %a\n]" (pp_list "\n " pp_coq_decl) ctxt @@ -125,10 +140,10 @@ let pp_fixpoint fmt (fp:(Constr.constr,Constr.types) Constr.pfixpoint) = let (rec_indices, i), (names, types, bodies) = fp in let n = Array.length names in let bodies = Array.init n (fun i -> (names.(i), types.(i), bodies.(i))) in - let pp_bodies fmt (n,t,b) = + let pp_bodies fmt (bind,t,b) = fprintf fmt "%a : %a :=@. %a," - pp_coq_name n pp_coq_term t pp_coq_term b in - fprintf fmt "Fix %a@. { %a }" pp_coq_name names.(i) (pp_array "@." pp_bodies) bodies + (pp_coq_binder pp_coq_name) bind pp_coq_term t pp_coq_term b in + fprintf fmt "Fix %a@. { %a }" (pp_coq_binder pp_coq_name) names.(i) (pp_array "@." pp_bodies) bodies let pp_coq_constraint fmt (i,rel,j) = diff --git a/src/debug.mli b/src/debug.mli index 8139e2c..b3693c3 100644 --- a/src/debug.mli +++ b/src/debug.mli @@ -59,11 +59,14 @@ val pp_coq_type : Constr.types printer val pp_coq_id : Names.Id.t printer val pp_coq_label : Names.Label.t printer val pp_coq_name : Names.Name.t printer +val pp_coq_binder : 'a printer -> 'a Context.binder_annot printer val pp_coq_kername : Names.KerName.t printer val pp_coq_sort : Sorts.t printer -val pp_coq_decl : Context.Rel.Declaration.t printer -val pp_coq_arity_ctxt : Context.Rel.Declaration.t list printer -val pp_coq_ctxt : Context.Rel.t printer +val pp_coq_decl : Constr.rel_declaration printer +val pp_coq_arity_ctxt : Constr.rel_declaration list printer +val pp_coq_ctxt : Constr.rel_context printer +val pp_coq_named_decl : Constr.named_declaration printer +val pp_coq_named_ctxt : Constr.named_context printer val pp_coq_env : Environ.env printer val pp_coq_level : Univ.Level.t printer val pp_coq_univ : Univ.Universe.t printer @@ -74,4 +77,4 @@ val pp_coq_constraint : Univ.univ_constraint printer val pp_coq_Constraint : Univ.Constraint.t printer val pp_coq_constraint_type : Univ.constraint_type printer val pp_uenv_cstr : (Univ.univ_constraint * (string * 'a) ) list printer -val pp_globname : Globnames.global_reference printer +val pp_globname : Names.GlobRef.t printer diff --git a/src/dune b/src/dune new file mode 100644 index 0000000..99c2ab8 --- /dev/null +++ b/src/dune @@ -0,0 +1,25 @@ +(library + (name coqine_plugin) ; This is the name you will use in + ; Coq's `Declare ML Module`, and + ; the name of the main OCaml + ; module of your plugin. + + (public_name coqine.plugin) ; This makes the plugin + ; installable; recommended, must + ; match opam package name + + (synopsis "Coqine Plugin") ; Synopsis, used in META generation + + (flags :standard -rectypes -w -27) ; Coq requires the `-rectypes` + ; flag; CoqPP generated code + ; requires to disable warning 27 + ; often. + + (libraries ; ML Libraries we want to link + ; with, your choice here. + coq.vernac ; needed for vernac extend + coq.plugins.ltac ; needed for tactic extend +)) + +; This will let Dune know about Coq's .mlg grammar files. +(coq.pp (modules commands)) diff --git a/src/encoding.ml b/src/encoding.ml index 2b7b6c4..9e39cd6 100644 --- a/src/encoding.ml +++ b/src/encoding.ml @@ -32,60 +32,61 @@ let set_params = List.iter (fun (x,y) -> set_param x y) let init_flags () = List.iter (fun (x,y) -> Hashtbl.replace flags x y) [ - ("simpl_letins" , false); - (** Translate let-in as simpl beta redices or not ? *) + ("simpl_letins" , false) + (* Translate let-in as simpl beta redices or not ? *) - ("upolymorphism" , false); - (** Is (true) polymorphism translation on ? *) + ; ("upolymorphism" , false) + (* Is (true) polymorphism translation on ? *) - ("tpolymorphism" , false); - (** Is template polymorphism translation on ? *) + ; ("tpolymorphism" , false) + (* Is template polymorphism translation on ? *) - ("tpoly_cons" , false); - (** Are template polymorphic constructors polymorphic ? *) + ; ("tpoly_cons" , false) + (* Are template polymorphic constructors polymorphic ? *) - ("tpoly_code" , false); - (** Should template polymorphic inductives parameter sort-irrelevance - be obtained through lift elimination (false) or a private code (true) ? *) + ; ("tpoly_code" , false) + (* Should template polymorphic inductives parameter sort-irrelevance + be obtained through lift elimination (false) or a private code (true) ? *) - ("float_univ" , false); - (** Is floating universe translation on ? *) + ; ("float_univ" , false) + (* Is floating universe translation on ? *) - ("constraints" , false); - (** Constraints translation ? Only has meaning when float is true. *) + ; ("constraints" , false) + (* Constraints translation ? Only has meaning when float is true. *) - ("named_univ" , false); - (** Should we use universe names or value ? Only has meaning when float is false. *) + ; ("named_univ" , false) + (* Should we use universe names or value ? + Only has meaning when float is false. *) - ("readable" , false); - (** Is (pseudo-)readable translation mode on ? *) + ; ("readable" , false) + (* Is (pseudo-)readable translation mode on ? *) - ("use_cast" , false); - (** Are we allowed to use casts (for casted lambdas) ? + ; ("use_cast" , false) + (* Are we allowed to use casts (for casted lambdas) ? Or should we turn them into lifted lambdas instead ? *) - ("pred_univ" , false); - ("pred_prod" , false); - ("pred_lift" , false); - ("pred_cast" , false); - ("priv_lift" , false); - ("priv_cast" , false); - ("priv_univ" , false); - ("priv_prod" , false); - - ("inlined_fixpoint", false); - (** Translate fixpoints as external body or inlined generic fixpoint operator ? + ; ("pred_univ" , false) + ; ("pred_prod" , false) + ; ("pred_lift" , false) + ; ("pred_cast" , false) + ; ("priv_lift" , false) + ; ("priv_cast" , false) + ; ("priv_univ" , false) + ; ("priv_prod" , false) + + ; ("inlined_fixpoint", false) + (* Translate fixpoints as external body or inlined generic fixpoint operator ? This is a very experimental feature. *) - ("fix_arity_sort" , false); + ; ("fix_arity_sort" , false) - ("cast_arguments" , false); - (** Should arguments of an application be systematically be casted to - their expected type ? *) + ; ("cast_arguments" , false) + (* Should arguments of an application be systematically be casted to + their expected type ? *) - ("code_guarded" , false); + ; ("code_guarded" , false) - ("unfold_letin" , false) + ; ("unfold_letin" , false) ] let init_empty_symbs () = @@ -109,6 +110,7 @@ let init_empty_symbs () = "cast"; (* Infinite hierarchy of universes constructors *) + "sprop"; "prop"; "set"; "type"; diff --git a/src/inductives.ml b/src/inductives.ml index 026a60a..4f7dceb 100644 --- a/src/inductives.ml +++ b/src/inductives.ml @@ -13,7 +13,7 @@ type ind_infos = (* [inductive_body] : a single inductive type definition, containing a name, an arity, and a list of constructor names and types *) - mind_univs : Declarations.abstract_inductive_universes; + mind_univs : Declarations.universes; (* Total number of mutually inductive types *) nb_mutind : int; @@ -24,6 +24,9 @@ type ind_infos = (* Body of the current inductive type *) body : Declarations.one_inductive_body; + (* Types with parameters *) + nf_full_types : Constr.types array; + (* Number of parameters common to all definitions *) n_params : int; @@ -37,11 +40,11 @@ type ind_infos = cons_names : Names.Id.t array; (* Full arity context (parameters and real arity together) *) - arity_context : Context.Rel.t; + arity_context : Constr.rel_context; (* Parameters context. Same for all mutual inductive definition. *) - mind_params_ctxt : Context.Rel.t; + mind_params_ctxt : Constr.rel_context; (* Real context. Specific to each mutual inductive definition. *) - arity_real_context : Context.Rel.t; + arity_real_context : Constr.rel_context; arity : Declarations.inductive_arity; @@ -79,6 +82,9 @@ let get_infos mind_body index = debug "--- Getting infos for inductive : %a ---" pp_coq_id typename; + let f (nf_ctxt,nf_type) = Term.it_mkProd_or_LetIn nf_type nf_ctxt in + let nf_full_types = Array.map f body.mind_nf_lc in + let arity_real_context, _ = Utils.list_chop body.mind_nrealdecls arity_context in (* Compute a map of template parameters and a sort for given declaration. *) @@ -92,14 +98,14 @@ let get_infos mind_body index = debug "Template level: %a" pp_coq_univ ta.template_level; debug "Arity context: %a" pp_coq_ctxt arity_context; Tsorts.translate_template_params ta.template_param_levels, - Term.Type ta.template_level + Sorts.sort_of_univ ta.template_level end in (* Compute universe polymorphic instance and associated constraints *) let apoly_ctxt, poly_ctxt, poly_inst, poly_cstr = match mind_univs with - | Monomorphic_ind univ_ctxt -> + | Monomorphic univ_ctxt -> Univ.AUContext.empty, Univ.UContext.empty, Univ.Instance.empty, @@ -107,13 +113,12 @@ let get_infos mind_body index = (* Univ.UContext.instance (Univ.ContextSet.to_context univ_ctxt), snd univ_ctxt *) - | Polymorphic_ind apoly_ctxt -> + | Polymorphic apoly_ctxt -> let poly_ctxt = Univ.AUContext.repr apoly_ctxt in apoly_ctxt, poly_ctxt, Univ.UContext.instance poly_ctxt, Univ.UContext.constraints poly_ctxt - | Cumulative_ind _ -> Error.not_supported "Mutual Cumulative inductive types" in let univ_poly_names = Tsorts.translate_univ_poly_params poly_inst in @@ -141,6 +146,7 @@ let get_infos mind_body index = nb_mutind; index; body; + nf_full_types; typename; arity_context; arity_real_context; @@ -165,15 +171,18 @@ let get_infos mind_body index = let is_template_parameter ind = function | Context.Rel.Declaration.LocalDef _ -> None - | Context.Rel.Declaration.LocalAssum (name, tp) -> + | Context.Rel.Declaration.LocalAssum (x, tp) -> let rec aux acc t = match Constr.kind t with - | Term.Prod(x,a,t) -> aux (Cname.translate_name x::acc) t - | Term.Sort (Sorts.Type u) -> + | Constr.Prod(binda,a,t) -> + let name = Context.binder_name binda in + aux (Cname.translate_name name::acc) t + | Constr.Sort (Sorts.Type u) -> (match Univ.Universe.level u with | None -> None | Some lvl -> try let _ = Info.translate_template_arg ind.inductive_uenv lvl in + let name = Context.binder_name x in Some (name, List.rev acc, lvl, Tsorts.translate_template_name lvl) with Not_found -> None ) @@ -183,18 +192,21 @@ let is_template_parameter ind = function (** Extract the list of LocalAssums in a context in reverse order. *) let extract_rel_context info env = - let rec aux (env, acc) = function + let rec aux env acc = function | [] -> (env, acc) | decl :: l -> match Context.Rel.Declaration.to_tuple decl with | (x, None, a) -> - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, a)) env in - aux (new_env, x::acc) l + let decl = Context.Rel.Declaration.LocalAssum(x, a) in + let name = Context.binder_name x in + let new_env = Environ.push_rel decl env in + aux new_env (name::acc) l | (x, Some u, a) -> - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalDef(x, u, a)) env in - aux (new_env, acc) l + let decl = Context.Rel.Declaration.LocalDef(x, u, a) in + let new_env = Environ.push_rel decl env in + aux new_env acc l in - aux (env, []) + aux env [] (* Inductive can either be "True" Polymorphic (Level quantified with constraints) @@ -434,19 +446,18 @@ let translate_template_inductive_levels info env label ind = I s1 ... sk p1 ... pr aj1(y1...ykj) ... ajn(y1...ykj) *) let translate_constructors info env label ind = - let mind = Names.MutInd.make3 info.module_path Names.DirPath.empty label in + let mind = Names.MutInd.make2 info.module_path label in (* Substitute the inductive types as specified in the Coq code. *) let ind_subst = Inductive.ind_subst mind ind.mind_body ind.poly_inst in for j = 0 to ind.n_cons - 1 do let cons_name = ind.body.mind_consnames.(j) in - let cons_type = ind.body.mind_nf_lc.(j) in - let cons_type = Vars.substl ind_subst cons_type in + let nf_full_types = Vars.substl ind_subst ind.nf_full_types.(j) in debug "Translating inductive constructor: %a" pp_coq_id cons_name; - debug "Cons_type: %a" pp_coq_type cons_type; + debug "Cons_full_type: %a" pp_coq_type nf_full_types; let cons_name' = Cname.translate_element_name info env (Names.Label.of_id cons_name) in let poly_env = Environ.push_context ind.poly_ctxt env in - let cons_type' = Terms.translate_types info poly_env ind.constructor_uenv cons_type in + let cons_type' = Terms.translate_types info poly_env ind.constructor_uenv nf_full_types in let cons_type' = Tsorts.add_constructor_params ind.template_names ind.univ_poly_names ind.univ_poly_cstr cons_type' in debug "Cons_type: %a" Dedukti.pp_term cons_type'; @@ -532,10 +543,9 @@ end *) let translate_cumulative_constructors_subtyping info env label ind = match ind.mind_univs with - | Monomorphic_ind _ - | Polymorphic_ind _ -> () + | Monomorphic _ + | Polymorphic _ -> () (* Constructor subtyping is only required for Cumulative Inductive types. *) - | Cumulative_ind _ -> assert false @@ -568,7 +578,7 @@ let translate_match info env label ind = let mind_body = ind.mind_body in let univ_instance = ind.poly_inst in - let mind = Names.MutInd.make3 info.module_path Names.DirPath.empty label in + let mind = Names.MutInd.make2 info.module_path label in let ind_term = Constr.mkIndU((mind, ind.index), ind.poly_inst) in let ind_subst = Inductive.ind_subst mind mind_body univ_instance in @@ -582,26 +592,58 @@ let translate_match info env label ind = let match_function_var' = Dedukti.var match_function_name' in debug "### %s" match_function_name'; - (* Use the normalized types in the rest. *) - let cons_types = Array.map (Vars.substl ind_subst) ind.body.mind_nf_lc in - let cons_context_types = Array.map Term.decompose_prod_assum cons_types in + (* Use the normalized types in the rest. + let sub (ctx,c) = + Context.Rel.map (Vars.substl ind_subst) ctx, Vars.substl ind_subst c in + let cons_nf_lc = Array.map sub ind.body.mind_nf_lc in + *) + + (* This is the applied inductive built by the constructor : Pair A B + let cons_types = Array.map snd cons_nf_lc in + *) + + (* This is the constructors full contexts (params + real arguments) : + [ (A:Prop) , (B:Prop) , (_:A) , (_:B) ] + let cons_contexts = Array.map fst cons_nf_lc in + *) + + (* This is the constructors full type (with params + real arguments) : + (A:Prop) -> (B:Prop) -> A -> B -> Pair A B + let cons_full_types = ind.nf_full_types in + *) (* Translate the match function: match_I *) let params_context = ind.mind_params_ctxt in let arity_real_context = ind.arity_real_context in - let ind_applied = Terms.apply_rel_context ind_term (arity_real_context @ params_context) in - let cons_contexts = Array.map fst cons_context_types in - let cons_types = Array.map snd cons_context_types in - let cons_real_contexts = Array.init ind.n_cons (fun j -> - fst (Utils.list_chop ind.body.mind_consnrealdecls.(j) cons_contexts.(j))) in - let cons_ind_args = Array.map - (fun a -> snd (Constr.decompose_app (Reduction.whd_all env a))) cons_types in + let ind_applied = Terms.apply_rel_context ind_term + (arity_real_context @ params_context) in + + let subst_nf_lc = + Array.init ind.n_cons (fun i -> + let (ctx, cty) = ind.body.mind_nf_lc.(i) in + let cty = Term.it_mkProd_or_LetIn cty ctx in + Term.decompose_prod_assum (Vars.substl ind_subst cty)) + in + + let cons_real_contexts = + Array.init ind.n_cons + (fun i -> fst (Utils.list_chop ind.body.mind_consnrealdecls.(i) + (fst subst_nf_lc.(i)))) + in + debug "Params ctxt: %a" pp_coq_ctxt params_context; + debug "Real ctxt: %a" (pp_array ", " pp_coq_ctxt) cons_real_contexts; + + let dec a = snd (Constr.decompose_app (Reduction.whd_all env (snd a))) in + let cons_ind_args = Array.map dec subst_nf_lc in + let cons_ind_real_args = Array.init ind.n_cons (fun j -> snd (Utils.list_chop ind.n_params cons_ind_args.(j))) in - let cons_applieds = Array.init ind.n_cons (fun j -> - Terms.apply_rel_context cons_terms.(j) (cons_real_contexts.(j) @ params_context)) in + let cons_applieds = + Array.init ind.n_cons (fun j -> + Terms.apply_rel_context cons_terms.(j) + (cons_real_contexts.(j) @ params_context)) in + debug "Ok: %a " (pp_array ", " pp_coq_term) cons_applieds; - if ind.n_cons > 0 then debug "Test: %a" pp_coq_term cons_applieds.(0); let params_env, params_context' = let global_env_with_poly = Environ.push_context ind.poly_ctxt (Global.env ()) in Terms.translate_rel_context info global_env_with_poly uenv params_context in @@ -642,10 +684,10 @@ let translate_match info env label ind = let matched_name' = Cname.translate_identifier matched_name in let matched_var' = Dedukti.var matched_name' in let params_env = Cname.push_identifier matched_name params_env in - let cases' = Array.map Dedukti.var case_names' in let params' = List.map Dedukti.var (fst (List.split params_context')) in + debug "Test: %a " (pp_array " / " (pp_list ", " pp_coq_decl)) cons_real_contexts; let cons_real_env_contexts' = Array.map (Terms.translate_rel_context info params_env uenv) @@ -657,17 +699,20 @@ let translate_match info env label ind = debug "Env: %a" pp_coq_env params_env; Array.iter (debug "%a" pp_coq_ctxt) cons_real_contexts; Array.iter (debug "%a" pp_coq_env ) cons_real_envs; + debug "ok"; let cons_ind_real_args' = Array.mapi (fun j -> Terms.translate_args info cons_real_envs.(j) uenv) cons_ind_real_args in + debug "ok"; let cons_applieds' = Array.mapi (fun j -> Terms.translate_constr info cons_real_envs.(j) uenv) cons_applieds in + debug "ok"; let aux = Encoding.flag "cast_arguments" in Encoding.set_flag "cast_arguments" false; @@ -929,9 +974,8 @@ end Only for a Cumulative Inductive Type with invariant sorts (WIP) *) match ind.mind_univs with - | Monomorphic_ind _ - | Polymorphic_ind _ -> () - | Cumulative_ind _ -> assert false + | Monomorphic _ + | Polymorphic _ -> () let translate_guarded info env label ind = @@ -978,8 +1022,10 @@ let translate_match_subtyping info env label ind = () let print_all_alias_symbols info env label alias = + (* let label' = Cname.translate_element_name info env label in let alias' = Cname.translate_kernel_name info env alias in let print (label', alias') = Dedukti.print info.fmt (Dedukti.alias label' alias') in + *) () diff --git a/src/info.ml b/src/info.ml index 8115f08..8283f74 100644 --- a/src/info.ml +++ b/src/info.ml @@ -44,7 +44,8 @@ let fetch_constraint uenv cstr = with Not_found -> None let fetch_higher_sorts uenv u = - let rec assoc acc ((i,c,j),(b,_,_)) = if compare i u = 0 then (c,j,b)::acc else acc + let assoc acc ((i,c,j),(b,_,_)) = + if compare i u = 0 then (c,j,b)::acc else acc (* FIXME: Equality constraints are not handled correctly here. - They should be considered both way - We should also prevent loops somehow *) diff --git a/src/libraries.ml b/src/libraries.ml index 15466f8..8d8c5d7 100644 --- a/src/libraries.ml +++ b/src/libraries.ml @@ -3,8 +3,21 @@ open Debug open Translator -(** Translate the library referred to by [qualid]. - A libray is a module that corresponds to a file on disk. **) +let translate_term term = + (* + let t = CAst.with_val (fun x -> x) term in + debug "Exporting %a" pp_coq_term t; + let module_path = assert false in + let filename = assert false in + let empty_env = assert false in + let info = assert false in + let term' = Terms.translate_constr info (Global.env ()) empty_env term in + Info.close info; +*) + Feedback.msg_notice (Pp.str "Dedukti rep: ") + +(* Translate the library referred to by [qualid]. + A libray is a module that corresponds to a file on disk. *) let translate_qualified_library qualid = let libname = Libnames.pr_qualid qualid in message "Exporting %a" pp_t libname; @@ -23,11 +36,8 @@ let translate_qualified_library qualid = debug_stop (); Info.close info -let qualid_of_ref r = (Libnames.qualid_of_reference r).CAst.v - -(** Translates the given library *) -let translate_library reference = - let qualid = qualid_of_ref reference in +(* Translates the given library *) +let translate_library qualid = let lib_loc, lib_path, lib_phys_path = Library.locate_qualified_library qualid in Library.require_library_from_dirpath [ (lib_path, Libnames.string_of_qualid qualid) ] None; Tsorts.set_universes (Global.universes ()); @@ -46,10 +56,9 @@ let translate_universes () = end; Info.close info -(** Translate all loaded libraries but expressions. **) -let translate_all_but refs = +(* Translate all loaded libraries but expressions. *) +let translate_all_but ignore_qualids = let sep = "\n Ignoring " in - let ignore_qualids = List.map qualid_of_ref refs in begin match ignore_qualids with | [] -> message "Translating all libraries" @@ -57,40 +66,13 @@ let translate_all_but refs = message "Translating all libraries except from the following:%s%a" sep (pp_list sep pp_t) (List.map Libnames.pr_qualid ignore_qualids) end; - let not_ignored qualid = not (List.exists (Libnames.qualid_eq qualid) ignore_qualids) in + let not_ignored qualid = + not (List.exists (Libnames.qualid_eq qualid) ignore_qualids) in let dirpaths = Library.loaded_libraries () in let qualids = List.map Libnames.qualid_of_dirpath dirpaths in Tsorts.set_universes (Global.universes ()); translate_universes (); List.iter translate_qualified_library (List.filter not_ignored qualids) -(** Translate all loaded libraries. **) +(* Translate all loaded libraries. *) let translate_all () = translate_all_but [] - - -let print_universes_constraints universes = - let register constraint_type j k = - match constraint_type with - | Univ.Lt -> message "%s < %s" j k - | Univ.Le -> message "%s <= %s" j k - | Univ.Eq -> message "%s == %s" j k - in - UGraph.dump_universes register universes - -let show_universes_constraints () = - message ""; - message "------------------------------------------------"; - message "| Printing global universes constraints |"; - message "------------------------------------------------"; - print_universes_constraints (Global.universes ()); - message "-----------------------------------------------"; - message "" - -let show_sorted_universes_constraints () = - message ""; - message "------------------------------------------------"; - message "| Printing global sorted universes constraints |"; - message "------------------------------------------------"; - print_universes_constraints (UGraph.sort_universes (Global.universes ())); - message "-----------------------------------------------"; - message "" diff --git a/src/libraries.mli b/src/libraries.mli index 4de4f12..441b4ef 100644 --- a/src/libraries.mli +++ b/src/libraries.mli @@ -1,9 +1,13 @@ (** Translation of Coq libraries *) -val translate_qualified_library : Libnames.qualid -> unit +val translate_term : Constr.t CAst.t -> unit +(** Translate a single Coq term to a string + (in an empty context, global environment). +*) + +val translate_library : Libnames.qualid -> unit -(** Translates the given library *) -val translate_library : Libnames.reference -> unit +val translate_qualified_library : Libnames.qualid -> unit (** Translate the universe table into the "U.dk" file Depending on the parameters, it could be: @@ -17,8 +21,4 @@ val translate_universes : unit -> unit val translate_all : unit -> unit (** Translate all loaded libraries. **) -val translate_all_but : Libnames.reference list -> unit - -val show_universes_constraints : unit -> unit - -val show_sorted_universes_constraints : unit -> unit +val translate_all_but : Libnames.qualid list -> unit diff --git a/src/modules.ml b/src/modules.ml index 8507aeb..b817eb3 100644 --- a/src/modules.ml +++ b/src/modules.ml @@ -20,7 +20,6 @@ let isalias resolver kername = then None else Some can - let translate_alias_constant_body info env alias label const = let label' = Cname.translate_element_name info env label in debug "Translating constant alias %a -> %a" @@ -44,11 +43,11 @@ let translate_constant_body info env isalias label const = assert (List.length const.const_hyps = 0); let poly_ctxt, poly_inst, poly_cstr, env = match const.const_universes with - | Monomorphic_const uctxt -> + | Monomorphic uctxt -> debug "Translating monomorphic constant body: %s" name; let env' = Environ.push_context_set ~strict:true uctxt env in Univ.AUContext.empty, Univ.Instance.empty, Univ.Constraint.empty, env' - | Polymorphic_const univ_ctxt -> + | Polymorphic univ_ctxt -> let uctxt = Univ.AUContext.repr univ_ctxt in let env' = Environ.push_context ~strict:false uctxt env in let instance = Univ.UContext.instance uctxt in @@ -88,6 +87,7 @@ let translate_constant_body info env isalias label const = let constr' = Terms.translate_constr ~expected_type:const_type info env uenv constr in let constr' = Tsorts.add_poly_params_def univ_poly_params univ_poly_cstr constr' in Dedukti.print info.fmt (Dedukti.definition true label' const_type' constr') + | Primitive _ -> assert false end (** Translate the body of mutual inductive definitions [mind]. *) @@ -145,8 +145,8 @@ let translate_mutual_coinductive_body info env isalias label mind_body = (** Translate the body of non-recursive definitions when it's a record. *) let translate_record_body info env isalias label mind_body = match mind_body.mind_record with - | None -> Error.not_supported "Non-recursive translation" - | Some _ -> + | NotRecord | FakeRecord -> Error.not_supported "Non-recursive translation" + | PrimRecord _ -> debug "Translating record: %a" pp_coq_label label; translate_mutual_inductive_body info env isalias label mind_body @@ -230,9 +230,11 @@ and translate_structure_field_body info env resolver (label, sfb) = if not_filtered full_name then begin + (* try + *) verbose "-> %s" full_name; - let kername = Names.KerName.make2 info.module_path label in + let kername = Names.KerName.make info.module_path label in match sfb with | SFBconst cb -> translate_constant_body info env (isalias resolver kername) label cb @@ -244,10 +246,12 @@ and translate_structure_field_body info env resolver (label, sfb) = ) info env (isalias resolver kername) label mib; | SFBmodule mb -> translate_module_body (Info.update info label) env mb | SFBmodtype _ -> () + (* with e -> if !fail_on_issue then (Info.close info; raise e) else verbose "[Error] On symbol %s: %s" full_name (Printexc.to_string e) + *) end else begin diff --git a/src/terms.ml b/src/terms.ml index 4f63c9b..c05509c 100644 --- a/src/terms.ml +++ b/src/terms.ml @@ -57,16 +57,15 @@ let fixpoint_signature env rec_decl = let fixpoint_signature env rec_decl = (env, rec_decl) - let translate_rel_decl info env decl = match Context.Rel.Declaration.to_tuple decl with - | (x, None, a) -> - let x = Cname.fresh_name ~default:"_" info env x in + | (binda, None, a) -> + let x = Cname.fresh_name ~default:"_" info env (Context.binder_name binda) in let x' = Cname.translate_name x in - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, a)) env in + let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(binda, a)) env in (new_env, Some (x',a)) - | (x, Some u, a) -> - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalDef(x, u, a)) env in + | (binda, Some u, a) -> + let new_env = Environ.push_rel (Context.Rel.Declaration.LocalDef(binda, u, a)) env in (new_env, None) let rec translate_sort_to_univ uenv t = @@ -75,9 +74,6 @@ let rec translate_sort_to_univ uenv t = | CastType (a', _) -> translate_sort_to_univ uenv a' | _ -> assert false -(** Infer and translate the sort of [a]. - Coq fails if we try to type a sort that was already inferred. - This function uses pattern matching to avoid it. *) let rec infer_translate_sort info env uenv a = (* This is wrong; there is no subject reduction in Coq! *) (* let a = Reduction.whd_all env a in*) @@ -87,10 +83,12 @@ let rec infer_translate_sort info env uenv a = They are never used in Coq's kernel but occur in SSReflect module *) | CastType(a', target) -> translate_sort_to_univ uenv target (* Error.not_supported "CastType" *) - | ProdType(x, a, b) -> - let x = Cname.fresh_name info env ~default:"_" x in + | ProdType(binda, a, b) -> + let name = Context.binder_name binda in + let name' = Cname.fresh_name info env ~default:"_" name in + let binda' = Context.make_annot name' Sorts.Relevant in let s1' = infer_translate_sort info env uenv a in - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, a)) env in + let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(binda', a)) env in let s2' = infer_translate_sort info new_env uenv b in Translator.Rule (s1',s2') | LetInType(x, u, a, b) -> @@ -99,7 +97,6 @@ let rec infer_translate_sort info env uenv a = infer_translate_sort info new_env uenv b | AtomicType _ -> Tsorts.translate_sort uenv (infer_sort env a) -(** Abstract over the variables of [context], eliminating let declarations. *) let abstract_rel_context context t = let abstract_rel_declaration t c = let (x, u, a) = (Context.Rel.Declaration.to_tuple c) in @@ -108,7 +105,6 @@ let abstract_rel_context context t = | Some(u) -> Vars.subst1 u t in List.fold_left abstract_rel_declaration t context -(** Generalize over the variables of [context], eliminating let declarations. *) let generalize_rel_context context b = let generalize_rel_declaration b c = let (x, u, a) = (Context.Rel.Declaration.to_tuple c) in @@ -117,15 +113,13 @@ let generalize_rel_context context b = | Some(u) -> Vars.subst1 u b in List.fold_left generalize_rel_declaration b context -(** Apply the variables of [context] to [t], ignoring let declarations. *) let apply_rel_context t context = - let apply_rel_declaration (args, i) c = - let (x, t, a) = (Context.Rel.Declaration.to_tuple c) in - match t with - | None -> (Constr.mkRel(i) :: args, i + 1) - | Some(_) -> (args, i + 1) in - let args, _ = List.fold_left apply_rel_declaration ([], 1) context in - Term.applistc t args + let apply_rel_declaration (args, i) = function + | Context.Rel.Declaration.LocalAssum _ -> + (Constr.mkRel(i) :: args, i + 1) + | Context.Rel.Declaration.LocalDef _ -> + (args, i + 1) in + Term.applistc t (fst (List.fold_left apply_rel_declaration ([], 1) context)) let rec convertible info env uenv a b = let a = Reduction.whd_all env a in @@ -151,45 +145,43 @@ let rec convertible info env uenv a b = end | _ -> false -(** This table holds the translations of fixpoints, so that we avoid - translating the same definition multiple times (e.g. mutual fixpoints). - This is very important, otherwise the size of the files will explode. *) +(* This table holds the translations of fixpoints, so that we avoid + translating the same definition multiple times (e.g. mutual fixpoints). + This is very important, otherwise the size of the files will explode. *) let fixpoint_table = Hashtbl.create 10007 let make_const mp x = - Names.Constant.make3 mp (Names.DirPath.make []) (Names.Label.of_id x) + Names.Constant.make2 mp (Names.Label.of_id x) -(** Use constant declarations instead of named variable declarations for lifted - terms because fixpoint declarations should be global and could be referred - to from other files (think Coq.Arith.Even with Coq.Init.Peano.plus). *) +(* Use constant declarations instead of named variable declarations for lifted + terms because fixpoint declarations should be global and could be referred + to from other files (think Coq.Arith.Even with Coq.Init.Peano.plus). *) let push_const_decl uenv env (c, m, const_type) = let const_body = match m with | None -> Undef None | Some m -> Def (Mod_subst.from_val m) in let const_body_code = - (** TODO : None does not handle polymorphic types ! *) + (* TODO : None does not handle polymorphic types ! *) match Cbytegen.compile_constant_body - ~fail_on_error:true - (Environ.pre_env env) - (Monomorphic_const Univ.ContextSet.empty) const_body with + ~fail_on_error:true env + (Monomorphic Univ.ContextSet.empty) const_body with | Some code -> code | None -> Error.error (Pp.str "compile_constant_body failed") in - (** TODO : Double check the following *) + (* TODO : Double check the following *) let body = { const_hyps = []; const_body = const_body; const_type = const_type; + const_relevance = Relevant; const_body_code = Some (Cemitcodes.from_val const_body_code); - const_universes = Polymorphic_const uenv.poly_ctxt; - const_proj = None; + const_universes = Polymorphic uenv.poly_ctxt; + const_private_poly_univs = None; const_inline_code = false; - const_typing_flags = - { check_guarded = false; - check_universes = false; - conv_oracle = Conv_oracle.empty - } + const_typing_flags = Declareops.safe_flags Conv_oracle.empty + (* FIXME: It's probably not best to use "safe" flags + for newly introduced constants... *) } in Environ.add_constant c body env @@ -229,11 +221,7 @@ let instantiate_universes env ctx ar argsorts = let safe_subst_fn x = try subst_fn x with | Not_found -> Univ.Universe.make x in let level = Univ.subst_univs_universe safe_subst_fn ar.template_level in - let ty = - if Univ.is_type0m_univ level then Sorts.prop - else if Univ.is_type0_univ level then Sorts.set - else Sorts.Type level - in (ctx,ty, subst, safe_subst_fn) + (ctx, Sorts.sort_of_univ level, subst, safe_subst_fn) let infer_ind_applied info env uenv (ind,u) args = debug "Inferring template polymorphic inductive: %a (%i)" @@ -248,7 +236,7 @@ let infer_ind_applied info env uenv (ind,u) args = let arity = Term.mkArity (List.rev ctx,s) in (* Do we really need to apply safe_subst to arity ? *) - let arity = Universes.subst_univs_constr subst arity in + let arity = UnivSubst.subst_univs_constr subst arity in debug "Substituted type: %a" pp_coq_term arity; arity, if Encoding.is_templ_polymorphism_on () @@ -275,7 +263,7 @@ let infer_construct_applied info env uenv ((ind,i),u) args = let ctx, s, subst, safe_subst = instantiate_universes env ctx ar args_types in debug "Subst: %a" pp_t (Univ.LMap.pr Univ.Universe.pr subst); if not (Encoding.is_templ_polymorphism_on ()) - then Universes.subst_univs_constr subst type_c, [] + then UnivSubst.subst_univs_constr subst type_c, [] else if not (Encoding.is_templ_polymorphism_cons_poly ()) then type_c, [] else @@ -289,7 +277,7 @@ let infer_construct_applied info env uenv ((ind,i),u) args = -> Univ.Instance.subst_fn -> Univ.Instance.of_array which assumes all substituted level are not Prop *) - Universes.subst_univs_constr subst type_c, + UnivSubst.subst_univs_constr subst type_c, List.map (fun lvl -> T.coq_universe (Tsorts.translate_universe uenv lvl)) (List.map safe_subst (Utils.filter_some ar.template_param_levels)) @@ -311,7 +299,7 @@ let infer_dest_applied info env uenv (ind,u) args = Encoding.is_templ_polymorphism_cons_poly () then (* Do we really need to apply safe_subst to arity ? *) - let arity = Universes.subst_univs_constr subst arity in + let arity = UnivSubst.subst_univs_constr subst arity in debug "Substituted type: %a" pp_coq_term arity; arity, List.map @@ -319,8 +307,6 @@ let infer_dest_applied info env uenv (ind,u) args = (List.map safe_subst (Utils.filter_some ar.template_param_levels)) else arity, [] - -(** Translate the Coq term [t] as a Dedukti term. *) let rec translate_constr ?expected_type info env uenv t = (* Check if the expected type coincides, otherwise make an explicit cast. *) let t = @@ -338,7 +324,7 @@ let rec translate_constr ?expected_type info env uenv t = let b = infer_type env t in debug " - Inferred: %a" (pp_coq_term_env env) b; if not (Encoding.is_argument_casted ()) && convertible info env uenv a b then t - else Constr.mkCast(t, Term.VMcast, a) in + else Constr.mkCast(t, Constr.VMcast, a) in match Constr.kind t with | Rel i -> let (x, u, _) = Context.Rel.Declaration.to_tuple (Environ.lookup_rel i env) in @@ -346,7 +332,7 @@ let rec translate_constr ?expected_type info env uenv t = | Some u -> (* If it's a let definition, replace by its value. *) translate_constr info env uenv (Vars.lift i u) - | None -> Dedukti.var (Cname.translate_name ~ensure_name:true x) + | None -> Dedukti.var (Cname.translate_binder x) end | Var x -> Dedukti.var (Cname.translate_identifier x) | Sort s -> T.coq_sort (Tsorts.translate_sort uenv s) @@ -355,38 +341,42 @@ let rec translate_constr ?expected_type info env uenv t = let t' = translate_constr info env uenv t in translate_cast info uenv t' env a env b - | Prod(x, a, b) -> - let x = Cname.fresh_name ~default:"_" info env x in + | Prod(binda, a, b) -> + let x = Cname.fresh_name ~default:"_" info env (Context.binder_name binda) in + let binda' = Context.make_annot x Sorts.Relevant in let x' = Cname.translate_name x in let a_sort = infer_translate_sort info env uenv a in let a' = translate_constr info env uenv a in let a'' = translate_types info env uenv a in - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, a)) env in + let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(binda', a)) env in let b_sort = infer_translate_sort info new_env uenv b in (* TODO: Should x really be in the environment when translating b's sort ? *) let b' = translate_constr info new_env uenv b in T.coq_prod a_sort b_sort a' (Dedukti.lam (x', a'') b') - | Lambda(x, a, t) -> - let x = Cname.fresh_name ~default:"_" info env x in + | Lambda(binda, a, t) -> + let x = Cname.fresh_name ~default:"_" info env (Context.binder_name binda) in let x' = Cname.translate_name x in + let binda' = Context.make_annot x Sorts.Relevant in let a'' = translate_types info env uenv a in - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, a)) env in + let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(binda', a)) env in let t' = translate_constr info new_env uenv t in Dedukti.lam (x', a'') t' | LetIn(x, u, a, t) -> if Encoding.is_letins_simpl () then - let id_x = match x with + let id_x = match Context.binder_name x with | Names.Name id -> id (* Assume letin var is named (otherwise what's the point ?) *) | Names.Anonymous -> assert false in let fresh_idx = Cname.fresh_identifier info env id_x in let x' = Cname.translate_identifier fresh_idx in let a' = translate_types info env uenv a in let u' = translate_constr info env uenv u in + let fresh_name = Names.Name.mk_name fresh_idx in + let fresh_binder = Context.make_annot fresh_name Sorts.Relevant in let def = Context.Rel.Declaration.LocalDef - (Names.Name.mk_name fresh_idx, Constr.mkVar fresh_idx, a) in + (fresh_binder, Constr.mkVar fresh_idx, a) in (* TODO: This is unsafe, the constant should also be pushed to the environment with its correct type *) let new_env = Environ.push_rel def env in @@ -471,7 +461,9 @@ let rec translate_constr ?expected_type info env uenv t = let n = Array.length names in debug "Translating %i fixpoints:" n; for i = 0 to n - 1 do - debug "%i -> %a : %a" i pp_coq_name names.(i) pp_coq_term types.(i); + debug "%i -> %a : %a" i + (pp_coq_binder pp_coq_name) names.(i) + pp_coq_term types.(i); debug "body: %a" pp_coq_term bodies.(i); done; (* TODO: not the whole environment should be added here, only the relevant part @@ -539,16 +531,14 @@ let rec translate_constr ?expected_type info env uenv t = (* Not yet supported cases: *) | Proj (p,t) -> begin - let kn = Names.Projection.constant p in - let cb = Environ.lookup_constant kn env in (* Constant body *) - let pb = Option.get cb.const_proj in (* Projection body *) - let n = pb.proj_arg in (* Index of the projection *) + let n = Names.Projection.arg p in (* Index of the projection *) T.coq_proj n (translate_constr info env uenv t) end (* Not supported cases: *) | Meta metavariable -> Error.not_supported "Meta" | Evar pexistential -> Error.not_supported "Evar" | CoFix(pcofixpoint) -> Error.not_supported "CoFix" + | Int _ -> Error.not_supported "Int" and translate_cast info uenv t' enva a envb b = debug "Casting %a@.from %a@.to %a" Dedukti.pp_term t' pp_coq_term a pp_coq_term b; @@ -617,9 +607,9 @@ and translate_cast info uenv t' enva a envb b = | _, CastType(b',_) -> translate_cast info uenv t' enva a envb b' (* Error.not_supported "CastType" *) - | ProdType(x1, a1, b1), ProdType(x2, a2, b2) -> + | ProdType(bind1, a1, b1), ProdType(x2, a2, b2) -> (* TODO: should we check for useless casts (b1~b2) ? *) - let x1' = Cname.fresh_name info enva x1 in + let x1, bind1 = Cname.fresh info enva bind1 in let (x,tA),t = match t' with | Dedukti.Lam ((x,Some tA),t) -> ((x,tA), t) @@ -627,16 +617,16 @@ and translate_cast info uenv t' enva a envb b = let tA = translate_types info enva uenv a1 in (* We assume a1 and a2 are convertible. Otherwise Coq's typecheking would have failed. *) - let x = Cname.translate_name x1' in - let t = Dedukti.app t' (Dedukti.var x) in - ((x,tA), t) + let x1' = Cname.translate_name x1 in + let t = Dedukti.app t' (Dedukti.var x1') in + ((x1',tA), t) in - let nenva = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x1', a1)) enva in - let nenvb = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x1', a2)) envb in + let decl = Context.Rel.Declaration.LocalAssum(bind1, a1) in + let nenva = Environ.push_rel decl enva in + let nenvb = Environ.push_rel decl envb in Dedukti.lam (x, tA) (translate_cast info uenv t nenva b1 nenvb b2) | _ -> t' -(** Translate the Coq type [a] as a Dedukti type. *) and translate_types info env uenv a = (* Specialize on the type to get a nicer and more compact translation. *) match Term.kind_of_type a with @@ -645,26 +635,28 @@ and translate_types info env uenv a = They are never used in Coq's kernel but occur in SSReflect module *) | CastType(a', _) -> translate_types info env uenv a' (* Error.not_supported "CastType" *) - | ProdType(x, a, b) -> - let x = Cname.fresh_name info ~default:"_" env x in + | ProdType(bind, a, b) -> + let x, bind = Cname.fresh info ~default:"_" env bind in let x' = Cname.translate_name x in let a' = translate_types info env uenv a in - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, a)) env in + let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(bind, a)) env in let b' = translate_types info new_env uenv b in Dedukti.pie (x', a') b' | LetInType(x, u, a, b) -> if Encoding.is_letins_simpl () then - let id_x = match x with + let id_x = match Context.binder_name x with | Names.Name id -> id (* Assume letin var is named (otherwise what's the point ?) *) | Names.Anonymous -> assert false in let fresh_idx = Cname.fresh_identifier info env id_x in + let fresh_name = Names.Name.mk_name fresh_idx in + let fresh_binder = Context.make_annot fresh_name Sorts.Relevant in let x' = Cname.translate_identifier fresh_idx in let a' = translate_types info env uenv a in let u' = translate_constr info env uenv u in let def = Context.Rel.Declaration.LocalDef - (Names.Name.mk_name fresh_idx, Constr.mkVar fresh_idx, a) in + (fresh_binder, Constr.mkVar fresh_idx, a) in (* TODO: This is unsafe, the constant should also be pushed to the environment with its correct type *) let new_env = Environ.push_rel def env in @@ -681,12 +673,11 @@ and translate_types info env uenv a = T.coq_term s' a' - -(** Translation of Fix fi { f1 / k1 : A1 := t1, ..., fn / kn : An := tn } *) +(* Translation of Fix fi { f1 / k1 : A1 := t1, ..., fn / kn : An := tn } *) and translate_fixpoint info env uenv (fp:(Constr.constr,Constr.types) Constr.pfixpoint) sorts = - let (rec_indices, i), (names, types, bodies) = fp in + let (rec_indices, i), (binders, types, bodies) = fp in debug "Translating fixpoint:@.%a" pp_fixpoint fp; - let n = Array.length names in + let n = Array.length binders in (* List of all (si,ki, Ai') where Ai' is Ai translated in current context *) let arities' = Array.init n @@ -696,10 +687,10 @@ and translate_fixpoint info env uenv (fp:(Constr.constr,Constr.types) Constr.pfi translate_constr ~expected_type:sorts.(i) info env uenv types.(i) ) in (* Fresh names fi' for the fi *) - let fresh_names = Array.map (Cname.fresh_name ~default:"_" info env) names in - let names' = Array.map Cname.translate_name fresh_names in + let fresh_binders = Array.map (Cname.fresh_binder ~default:"_" info env) binders in + let names' = Array.map Cname.translate_binder fresh_binders in (* Computing the extended context where all recursive function symbols are added *) - let ext_env = Environ.push_rec_types (fresh_names,types,types) env in + let ext_env = Environ.push_rec_types (fresh_binders,types,types) env in (* Lifted Ai to represent the same term in the extended context *) let lifted_types = Array.map (fun ty -> Vars.lift n ty) types in (* Bodi ti is translated as f1' => ... fn' => ti' *) @@ -713,7 +704,8 @@ and translate_fixpoint info env uenv (fp:(Constr.constr,Constr.types) Constr.pfi and lift_let info env uenv x u a = - let y = Cname.fresh_of_name ~global:true ~prefix:"let" ~default:"_" info env x in + let name = Context.binder_name x in + let y = Cname.fresh_of_name ~global:true ~prefix:"let" ~default:"_" info env name in let yconstant = make_const info.module_path y in let y' = Cname.translate_constant info env yconstant in let rel_context = Environ.rel_context env in @@ -767,9 +759,9 @@ and lift_fix info env uenv names types bodies rec_indices = |[(fix1_f G)/f]t|. *) let n = Array.length names in - let fix_names1 = Array.map (Cname.fresh_of_name info env ~global:true ~prefix:"fix1" ~default:"_") names in - let fix_names2 = Array.map (Cname.fresh_of_name info env ~global:true ~prefix:"fix2" ~default:"_") names in - let fix_names3 = Array.map (Cname.fresh_of_name info env ~global:true ~prefix:"fix3" ~default:"_") names in + let fix_names1 = Array.map (Cname.fresh_of_name_binder info env ~global:true ~prefix:"fix1" ~default:"_") names in + let fix_names2 = Array.map (Cname.fresh_of_name_binder info env ~global:true ~prefix:"fix2" ~default:"_") names in + let fix_names3 = Array.map (Cname.fresh_of_name_binder info env ~global:true ~prefix:"fix3" ~default:"_") names in let contexts_return_types = Array.mapi (fun i -> Term.decompose_prod_n_assum (rec_indices.(i) + 1)) types in let contexts = Array.map fst contexts_return_types in let return_types = Array.map snd contexts_return_types in @@ -783,10 +775,15 @@ and lift_fix info env uenv names types bodies rec_indices = let arity_contexts = Array.map (fun body -> fst (Inductive.mind_arity body)) one_ind_body in let ind_applied_arities = Array.init n (fun i -> apply_rel_context (Constr.mkInd inds.(i)) arity_contexts.(i)) in let types1 = types in - let types2 = Array.init n (fun i -> - generalize_rel_context contexts.(i) ( - generalize_rel_context arity_contexts.(i) ( - Term.mkArrow ind_applied_arities.(i) (Vars.lift (List.length arity_contexts.(i) + 1) return_types.(i))))) in + let types2 = + Array.init n + (fun i -> + generalize_rel_context contexts.(i) + (generalize_rel_context arity_contexts.(i) + (Term.mkArrow + ind_applied_arities.(i) Sorts.Relevant + (Vars.lift (List.length arity_contexts.(i) + 1) return_types.(i))))) + in let types3 = types in let rel_context = Environ.rel_context env in let types1_closed = Array.map (generalize_rel_context rel_context) types1 in @@ -895,8 +892,6 @@ and lift_fix info env uenv names types bodies rec_indices = let env = Array.fold_left (push_const_decl uenv) env name3_declarations in env, fix_declarations1 -(** Translate the context [x1 : a1, ..., xn : an] into the list - [x1, ||a1||; ...; x1, ||an||], ignoring let declarations. *) and translate_rel_context info env uenv context = let aux decl (env, translated) = match translate_rel_decl info env decl with @@ -908,7 +903,6 @@ and translate_rel_context info env uenv context = (* Reverse the list as the newer declarations are on top. *) (env, List.rev translated) -(** Translating Constrs as Dedukti patterns *) let translate_args info env uenv ts = (* TODO: improve this to have patterns *) List.map (translate_constr info env uenv) ts diff --git a/src/terms.mli b/src/terms.mli index 252f149..acf3595 100644 --- a/src/terms.mli +++ b/src/terms.mli @@ -6,15 +6,21 @@ val infer_sort : Environ.env -> Constr.types -> Sorts.t val infer_translate_sort : Info.info -> Environ.env -> Info.env -> Constr.types -> Translator.universe_expr +(** Infer and translate the sort of [a]. + Coq fails if we try to type a sort that was already inferred. + This function uses pattern matching to avoid it. *) val abstract_rel_context : - Context.Rel.Declaration.t list -> Constr.t -> Constr.t + Constr.rel_context -> Constr.t -> Constr.t +(** Abstract over the variables of [context], eliminating let declarations. *) val generalize_rel_context : - Context.Rel.Declaration.t list -> Constr.types -> Constr.types + Constr.rel_context -> Constr.types -> Constr.types +(** Generalize over the variables of [context], eliminating let declarations. *) val apply_rel_context : - Constr.t -> Context.Rel.Declaration.t list -> Constr.t + Constr.t -> Constr.rel_context -> Constr.t +(** Apply the variables of [context] to [t], ignoring let declarations. *) val convertible : Info.info -> Environ.env -> Info.env -> Constr.t -> Constr.t -> bool @@ -24,17 +30,21 @@ val make_const : Names.ModPath.t -> Names.Id.t -> Names.Constant.t val translate_constr : ?expected_type:Constr.t -> Info.info -> Environ.env -> Info.env -> Constr.t -> Dedukti.term +(** Translate the Coq term [t] as a Dedukti term. *) val translate_types : Info.info -> Environ.env -> Info.env -> Constr.types -> Dedukti.term +(** Translate the Coq type [a] as a Dedukti type. *) val translate_rel_decl : Info.info -> Environ.env -> - Context.Rel.Declaration.t -> (Environ.env * (Dedukti.var * Constr.types) option) + Constr.rel_declaration -> (Environ.env * (Dedukti.var * Constr.types) option) val translate_rel_context : Info.info -> Environ.env -> Info.env -> - Context.Rel.t -> Environ.env * (Dedukti.var * Dedukti.term) list + Constr.rel_context -> Environ.env * (Dedukti.var * Dedukti.term) list +(** Translate the context [x1 : a1, ..., xn : an] into the list + [x1, ||a1||; ...; x1, ||an||], ignoring let declarations. *) val translate_args : Info.info -> Environ.env -> Info.env -> Constr.t list -> Dedukti.term list diff --git a/src/translator.ml b/src/translator.ml index 819a137..5826965 100644 --- a/src/translator.ml +++ b/src/translator.ml @@ -10,6 +10,7 @@ type level_expr = | Max of level_expr list type universe_expr = + | SProp | Prop | Set | Type of level_expr @@ -40,6 +41,7 @@ let coq_z = vsymbu "lvl0" let coq_succ s = app (coq_s()) s let coq_succs s i = Utils.iterate i coq_succ s let coq_nat n = coq_succs (coq_z()) n +let coq_sprop = vsymbu "sprop" let coq_prop = vsymbu "prop" let coq_set = vsymbu "set" let coq_type u = app (vsymb "type") u @@ -107,6 +109,7 @@ struct | [u] -> u | (u :: u_list) -> apps (vsymb "sup") [u; coq_sup u_list] let rec cu = function + | SProp -> coq_sprop () | Prop -> coq_prop () | Set -> coq_set () | Type lvl -> coq_type (cl lvl) diff --git a/src/translator.mli b/src/translator.mli index 9be09f2..2229083 100644 --- a/src/translator.mli +++ b/src/translator.mli @@ -13,8 +13,12 @@ type level_expr = (** Representation of universe expression *) type universe_expr = + | SProp + (** Impredicative sort-irrelevant SProp *) | Prop - | Set (** Predicative Set *) + (** Impredicative Prop *) + | Set + (** Predicative Set *) | Type of level_expr (** Type of a level *) | GlobalSort of string (** Global universe "Coq.Module.index" *) @@ -82,7 +86,9 @@ sig val coq_nat_universe : universe_expr -> term (** Nat level of universe *) + val coq_trans_cstr : term -> (term * term) list -> term + val coq_conj_cstr : (term * term) list -> term val coq_U : universe_expr -> term val coq_term : universe_expr -> term -> term @@ -108,6 +114,7 @@ sig val coq_pattern_lifted_from_sort : term -> term -> term (** [coq_pattern_lifted_from_sort s t] Returns a pattern matching a term lifted from sort pattern [s] (for instance a variable). *) + val coq_pattern_lifted_from_level : var -> term -> term (** [coq_pattern_lifted_from_level lvl t] Returns a pattern matching a term lifted from sort [type lvl] . *) diff --git a/src/tsorts.ml b/src/tsorts.ml index 0a85f45..860c2bd 100644 --- a/src/tsorts.ml +++ b/src/tsorts.ml @@ -231,8 +231,8 @@ let set_universes universes = let universes = UGraph.sort_universes universes in let register constraint_type j k = match constraint_type with - | Univ.Eq -> Scanf.sscanf k "Type.%d" - (fun k -> Hashtbl.add universe_table j (mk_level k)) + | Univ.Eq -> Scanf.sscanf (Univ.Level.to_string k) "Type.%d" + (fun k -> Hashtbl.add universe_table (Univ.Level.to_string j) (mk_level k)) | Univ.Lt | Univ.Le -> () in UGraph.dump_universes register universes end @@ -243,7 +243,7 @@ let translate_template_global_level_decl (ctxt:Univ.Level.t option list) = let params = Utils.filter_some ctxt in let aux l = match Univ.Level.name l with - | Some (d,n) -> + | Some _ -> let name = Univ.Level.to_string l in let name' = T.coq_univ_name name in if Encoding.is_float_univ_on () @@ -342,9 +342,10 @@ let translate_universe uenv u = | levels -> Translator.Sup levels let translate_sort uenv = function - | Term.Prop Sorts.Null -> Translator.Prop - | Term.Prop Sorts.Pos -> Translator.Set - | Term.Type i -> translate_universe uenv i + | Term.SProp -> Translator.SProp + | Term.Prop -> Translator.Prop + | Term.Set -> Translator.Set + | Term.Type i -> translate_universe uenv i let convertible_sort uenv s1 s2 = translate_sort uenv s1 = translate_sort uenv s2 @@ -380,7 +381,7 @@ let translate_univ_poly_constraints (uctxt:Univ.Constraint.t) = let translate_template_name l = match Univ.Level.name l with - | Some (d,n) -> T.coq_univ_name (Univ.Level.to_string l) + | Some _ -> T.coq_univ_name (Univ.Level.to_string l) | _ -> assert false (** Extracts template parameters levels and returns them with their dedukti names diff --git a/src/tsorts.mli b/src/tsorts.mli index 54dabe9..5c37006 100644 --- a/src/tsorts.mli +++ b/src/tsorts.mli @@ -120,6 +120,7 @@ val translate_univ_poly_params : Univ.Instance.t -> string list val translate_univ_poly_constraints : Univ.Constraint.t -> cstr list -val gather_eq_types : Context.Rel.t -> Context.Rel.t -> (Constr.types * Constr.types) list +val gather_eq_types : + Constr.rel_context -> Constr.rel_context -> (Constr.types * Constr.types) list val enforce_eq_types : Univ.Constraint.t -> (Constr.t * Constr.t) list -> Univ.Constraint.t diff --git a/src/tunivs.ml b/src/tunivs.ml index 0a2c481..ce098bd 100644 --- a/src/tunivs.ml +++ b/src/tunivs.ml @@ -10,8 +10,10 @@ let get_universes_levels (universes:UGraph.t) = let register constraint_type j k = match constraint_type with | Univ.Eq -> - let closed_univ = Scanf.sscanf k "Type.%d" (fun x -> x) in - res := (T.coq_univ_name j, Translator.mk_level closed_univ):: !res + let closed_univ = Scanf.sscanf (Univ.Level.to_string k) "Type.%d" (fun x -> x) in + (* Coq does not expose the (string*int) representation + of RawLavel's Levels named level so print-and-parse it for now *) + res := (T.coq_univ_name (Univ.Level.to_string j), Translator.mk_level closed_univ):: !res | Univ.Lt | Univ.Le -> () in UGraph.dump_universes register universes; !res @@ -23,14 +25,18 @@ module StringSet = Set.Make(struct type t = string let compare = String.compare let get_universes_constraints (universes:UGraph.t) = let defined_univs = ref StringSet.empty in let reg u = - if u = "Set" then set_level - else if u = "Prop" then set_level (* Hack to represent Prop as a level *) - else if Utils.str_starts_with "Type." u - then mk_level (Scanf.sscanf u "Type.%d" (fun x -> x)) - else begin - if not (StringSet.mem u !defined_univs) - then defined_univs := StringSet.add u !defined_univs; - Translator.GlobalLevel u + + if Univ.Level.is_set u then set_level + else if Univ.Level.is_prop u then set_level + (* Hack to represent Prop as a level even though it shouldn't *) + else + let u' = Univ.Level.to_string u in + if Utils.str_starts_with "Type." u' + then mk_level (Scanf.sscanf u' "Type.%d" (fun x -> x)) + else begin + if not (StringSet.mem u' !defined_univs) + then defined_univs := StringSet.add u' !defined_univs; + Translator.GlobalLevel u' end in let res = ref [] in From 82261f1c68d0fa3817c2998bcf781c3c91b1cb7b Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Thu, 6 Feb 2020 12:00:15 +0100 Subject: [PATCH 2/7] Fixed some bugs --- .travis.yml | 4 +- coqine.opam | 4 +- run/logipedia/Makefile | 7 +- run/upoly_logipedia/Makefile | 7 +- src/cname.ml | 4 +- src/cname.mli | 3 +- src/debug.ml | 6 +- src/inductives.ml | 13 +- src/modules.ml | 3 +- src/terms.ml | 314 +++++++++++++++++------------------ 10 files changed, 179 insertions(+), 186 deletions(-) diff --git a/.travis.yml b/.travis.yml index 3097b75..239037a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -17,7 +17,7 @@ env: - OPAMJOBS="2" - OPAMYES="true" - OPAMVERBOSE="true" - - OCAML_VERSION=4.06.0 + - OCAML_VERSION=4.09.0 before_install: # Obtain and install opam locally. @@ -38,8 +38,6 @@ install: script: - make plugin - - echo "Add ML Path \"$(pwd)/src\"." >> $HOME/.coqrc - - cat $HOME/.coqrc - make -C encodings - make - make tests diff --git a/coqine.opam b/coqine.opam index 349c52d..248df3f 100644 --- a/coqine.opam +++ b/coqine.opam @@ -9,8 +9,8 @@ bug-reports: "https://github.com/Deducteam/CoqInE/" dev-repo: "git+https://github.com/Deducteam/CoqInE" license: "GPL 3" depends: [ - "ocaml" { >= "4.04.0" } - "coq" { = "8.8.2" } + "ocaml" { >= "4.09.0" } + "coq" { = "8.10.0" } "dune" { build & >= "1.9.0" } ] build: [ "dune" "build" "-p" name "-j" jobs ] diff --git a/run/logipedia/Makefile b/run/logipedia/Makefile index bb27e49..dd07885 100644 --- a/run/logipedia/Makefile +++ b/run/logipedia/Makefile @@ -2,14 +2,15 @@ # Variables COQ_MAKEFILE ?= coq_makefile -COQC ?= coqc +COQC ?= coqc -allow-sprop DKCHECK ?= dkcheck DKDEP ?= dkdep VERBOSE ?= MAINFILE ?= main OUTFOLDER = out -COQINEPATH=../../src +COQINE_SRC=../../src/ +COQINE_LIB=../../_build/install/default/lib/coqine/plugin/ DKS = $(wildcard $(OUTFOLDER)/*.dk) DKOS = $(DKS:.dk=.dko) @@ -33,7 +34,7 @@ $(OUTFOLDER): # Generate the [.dk] files by executing [main_???.v] generate: compile $(OUTFOLDER) - $(COQC) -nois -init-file ../../.coqrc -verbose -R . Top $(MAINFILE).v + $(COQC) -nois -verbose -R . Top -Q $(COQINE_SRC) Coqine -I $(COQINE_LIB) $(MAINFILE).v # Generate the dependencies of [.dk] files depend: diff --git a/run/upoly_logipedia/Makefile b/run/upoly_logipedia/Makefile index bb27e49..dd07885 100644 --- a/run/upoly_logipedia/Makefile +++ b/run/upoly_logipedia/Makefile @@ -2,14 +2,15 @@ # Variables COQ_MAKEFILE ?= coq_makefile -COQC ?= coqc +COQC ?= coqc -allow-sprop DKCHECK ?= dkcheck DKDEP ?= dkdep VERBOSE ?= MAINFILE ?= main OUTFOLDER = out -COQINEPATH=../../src +COQINE_SRC=../../src/ +COQINE_LIB=../../_build/install/default/lib/coqine/plugin/ DKS = $(wildcard $(OUTFOLDER)/*.dk) DKOS = $(DKS:.dk=.dko) @@ -33,7 +34,7 @@ $(OUTFOLDER): # Generate the [.dk] files by executing [main_???.v] generate: compile $(OUTFOLDER) - $(COQC) -nois -init-file ../../.coqrc -verbose -R . Top $(MAINFILE).v + $(COQC) -nois -verbose -R . Top -Q $(COQINE_SRC) Coqine -I $(COQINE_LIB) $(MAINFILE).v # Generate the dependencies of [.dk] files depend: diff --git a/src/cname.ml b/src/cname.ml index 892d53e..e539185 100644 --- a/src/cname.ml +++ b/src/cname.ml @@ -116,9 +116,9 @@ let escape name = let translate_identifier identifier = escape (Names.Id.to_string identifier) -let translate_name = function +let translate_name ?(ensure_name=false) = function | Names.Name(identifier) -> translate_identifier identifier - | Names.Anonymous -> failwith "Anonymous name" + | Names.Anonymous -> if ensure_name then failwith "Anonymous name" else "" let translate_binder b = translate_name (Context.binder_name b) diff --git a/src/cname.mli b/src/cname.mli index c6cfa3f..3281728 100644 --- a/src/cname.mli +++ b/src/cname.mli @@ -51,10 +51,9 @@ val is_alpha_numerical : char -> bool val escape : string -> string - val translate_identifier : Names.Id.t -> string -val translate_name : Names.Name.t -> string +val translate_name : ?ensure_name:bool -> Names.Name.t -> string val translate_binder : Names.Name.t Context.binder_annot -> string diff --git a/src/debug.ml b/src/debug.ml index 585e207..45f5b9a 100644 --- a/src/debug.ml +++ b/src/debug.ml @@ -66,11 +66,7 @@ let printer_of_std_ppcmds f fmt x = fprintf fmt "%a" pp_t (f x) let pp_coq_term_env env = printer_of_std_ppcmds (Printer.safe_pr_constr_env env (Evd.from_env env)) - -let pp_coq_term = - let env = Global.env () in - let sigma = Evd.from_env env in - printer_of_std_ppcmds (Printer.safe_pr_constr_env env sigma) +let pp_coq_term = pp_coq_term_env (Global.env()) let pp_coq_type = let env = Global.env () in let sigma = Evd.from_env env in diff --git a/src/inductives.ml b/src/inductives.ml index 4f7dceb..5c25a9e 100644 --- a/src/inductives.ml +++ b/src/inductives.ml @@ -74,6 +74,7 @@ let get_infos mind_body index = let n_params = mind_body.mind_nparams in let mind_univs = mind_body.mind_universes in let mind_params_ctxt = mind_body.mind_params_ctxt in + debug "mind_params: %a" pp_coq_ctxt mind_params_ctxt; let typename = body.mind_typename in let arity_context = body.mind_arity_ctxt in let arity = body.mind_arity in @@ -245,6 +246,7 @@ let translate_inductive info env label ind = let arity' = Tsorts.add_inductive_params ind.template_names ind.univ_poly_names ind.univ_poly_cstr arity' in (* Printing out the type declaration. *) + debug "ok"; let definable = Encoding.is_templ_polymorphism_ind_code() || List.exists (fun p -> Option.has_some (is_template_parameter ind p)) ind.mind_params_ctxt @@ -638,11 +640,9 @@ let translate_match info env label ind = let cons_ind_real_args = Array.init ind.n_cons (fun j -> snd (Utils.list_chop ind.n_params cons_ind_args.(j))) in - let cons_applieds = - Array.init ind.n_cons (fun j -> - Terms.apply_rel_context cons_terms.(j) - (cons_real_contexts.(j) @ params_context)) in - debug "Ok: %a " (pp_array ", " pp_coq_term) cons_applieds; + let cons_applieds = Array.init ind.n_cons (fun j -> + Terms.apply_rel_context cons_terms.(j) (cons_real_contexts.(j) @ params_context)) in + debug "Cons applieds: %a " (pp_array ", " pp_coq_term) cons_applieds; let params_env, params_context' = let global_env_with_poly = Environ.push_context ind.poly_ctxt (Global.env ()) in @@ -705,7 +705,8 @@ let translate_match info env label ind = Array.mapi (fun j -> Terms.translate_args info cons_real_envs.(j) uenv) cons_ind_real_args in - debug "ok"; + + debug "Real envs : %a" (pp_array "\n" pp_coq_env) cons_real_envs; let cons_applieds' = Array.mapi diff --git a/src/modules.ml b/src/modules.ml index b817eb3..685697b 100644 --- a/src/modules.ml +++ b/src/modules.ml @@ -145,7 +145,8 @@ let translate_mutual_coinductive_body info env isalias label mind_body = (** Translate the body of non-recursive definitions when it's a record. *) let translate_record_body info env isalias label mind_body = match mind_body.mind_record with - | NotRecord | FakeRecord -> Error.not_supported "Non-recursive translation" + | NotRecord + | FakeRecord | PrimRecord _ -> debug "Translating record: %a" pp_coq_label label; translate_mutual_inductive_body info env isalias label mind_body diff --git a/src/terms.ml b/src/terms.ml index c05509c..2971f59 100644 --- a/src/terms.ml +++ b/src/terms.ml @@ -57,16 +57,12 @@ let fixpoint_signature env rec_decl = let fixpoint_signature env rec_decl = (env, rec_decl) -let translate_rel_decl info env decl = - match Context.Rel.Declaration.to_tuple decl with - | (binda, None, a) -> - let x = Cname.fresh_name ~default:"_" info env (Context.binder_name binda) in - let x' = Cname.translate_name x in - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(binda, a)) env in - (new_env, Some (x',a)) - | (binda, Some u, a) -> - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalDef(binda, u, a)) env in - (new_env, None) +let translate_rel_decl info env = function + | Context.Rel.Declaration.LocalAssum (binda, a) -> + let fresh_name, fresh_binder = Cname.fresh ~default:"_" info env binda in + ( Environ.push_rel (Context.Rel.Declaration.LocalAssum(fresh_binder, a)) env, + Some (Cname.translate_name fresh_name, a)) + | decl -> (Environ.push_rel decl env, None) let rec translate_sort_to_univ uenv t = match Term.kind_of_type t with @@ -84,17 +80,15 @@ let rec infer_translate_sort info env uenv a = | CastType(a', target) -> translate_sort_to_univ uenv target (* Error.not_supported "CastType" *) | ProdType(binda, a, b) -> - let name = Context.binder_name binda in - let name' = Cname.fresh_name info env ~default:"_" name in - let binda' = Context.make_annot name' Sorts.Relevant in - let s1' = infer_translate_sort info env uenv a in - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(binda', a)) env in - let s2' = infer_translate_sort info new_env uenv b in - Translator.Rule (s1',s2') + let name', binda' = Cname.fresh info env ~default:"_" binda in + let s1' = infer_translate_sort info env uenv a in + let new_env = Environ.push_rel (Context.Rel.Declaration.LocalAssum(binda', a)) env in + let s2' = infer_translate_sort info new_env uenv b in + Translator.Rule (s1',s2') | LetInType(x, u, a, b) -> - (* No need to lift the let here. *) - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalDef(x, u, a)) env in - infer_translate_sort info new_env uenv b + (* No need to lift the let here. *) + let new_env = Environ.push_rel (Context.Rel.Declaration.LocalDef(x, u, a)) env in + infer_translate_sort info new_env uenv b | AtomicType _ -> Tsorts.translate_sort uenv (infer_sort env a) let abstract_rel_context context t = @@ -363,20 +357,19 @@ let rec translate_constr ?expected_type info env uenv t = let t' = translate_constr info new_env uenv t in Dedukti.lam (x', a'') t' - | LetIn(x, u, a, t) -> + | LetIn(binda, u, a, t) -> if Encoding.is_letins_simpl () then - let id_x = match Context.binder_name x with - | Names.Name id -> id (* Assume letin var is named (otherwise what's the point ?) *) + let fresh_name, fresh_binder = Cname.fresh info env binda in + let fresh_id = match fresh_name with + | Names.Name id -> id + (* Assume letin var is named (otherwise what's the point ?) *) | Names.Anonymous -> assert false in - let fresh_idx = Cname.fresh_identifier info env id_x in - let x' = Cname.translate_identifier fresh_idx in + let x' = Cname.translate_identifier fresh_id in let a' = translate_types info env uenv a in let u' = translate_constr info env uenv u in - let fresh_name = Names.Name.mk_name fresh_idx in - let fresh_binder = Context.make_annot fresh_name Sorts.Relevant in let def = Context.Rel.Declaration.LocalDef - (fresh_binder, Constr.mkVar fresh_idx, a) in + (fresh_binder, Constr.mkVar fresh_id, a) in (* TODO: This is unsafe, the constant should also be pushed to the environment with its correct type *) let new_env = Environ.push_rel def env in @@ -384,149 +377,151 @@ let rec translate_constr ?expected_type info env uenv t = let t' = translate_constr info new_env uenv t in Dedukti.letin (x',u',a') t' with Type_errors.TypeError _ | Constr.DestKO -> - let new_env = lift_let info env uenv x u a in + let new_env = lift_let info env uenv binda u a in translate_constr info new_env uenv t else - let new_env = lift_let info env uenv x u a in + let new_env = lift_let info env uenv binda u a in translate_constr info new_env uenv t | App(f, args) -> - debug "App: %a [%n]" (pp_coq_term_env env) f (Array.length args); - Array.iteri (fun i t -> debug "Arg %n : %a" i (pp_coq_term_env env) t) args; - let tmpl_args = if Encoding.is_templ_polymorphism_on () then args else [||] in - let type_f, template_univ_parameters = - match Constr.kind f with - (* Template Polymorphic Inductive Constructions require the given parameters - to compute the proper universe instance (and univ parameters). *) - | Ind (ind, u) -> - infer_ind_applied info env uenv (ind,u) tmpl_args - | Construct ((ind, c), u) -> - infer_construct_applied info env uenv ((ind, c), u) tmpl_args - (* "True" Polymorphic Constants *) - (* - | Const (cst,u) when Environ.polymorphic_pconstant (cst,u) env -> - debug "Instance: %a" pp_coq_inst u; - Environ.constant_type_in env (cst,u), [] - *) - | _ -> infer_type env f, [] - in - let f' = Dedukti.apps (translate_constr info env uenv f) template_univ_parameters in - let translate_app (f', type_f) u = - debug "Type f : %a" (pp_coq_term_env env) type_f; - let _, c, d = Constr.destProd (Reduction.whd_all env type_f) in - let u' = translate_constr ~expected_type:c info env uenv u in - (Dedukti.app f' u', Vars.subst1 u d) in - fst (Array.fold_left translate_app (f', type_f) args) + debug "Env: %a" pp_coq_env env; + debug "App: %a [%n]" (pp_coq_term_env env) f (Array.length args); + Array.iteri (fun i t -> debug "Arg %n : %a" i (pp_coq_term_env env) t) args; + let tmpl_args = if Encoding.is_templ_polymorphism_on () then args else [||] in + let type_f, template_univ_parameters = + match Constr.kind f with + (* Template Polymorphic Inductive Constructions require the given parameters + to compute the proper u niverse instance (and univ parameters). *) + | Ind (ind, u) -> + infer_ind_applied info env uenv (ind,u) tmpl_args + | Construct ((ind, c), u) -> + infer_construct_applied info env uenv ((ind, c), u) tmpl_args + (* "True" Polymorphic Constants *) + (* + | Const (cst,u) when Environ.polymorphic_pconstant (cst,u) env -> + debug "Instance: %a" pp_coq_inst u; + Environ.constant_type_in env (cst,u), [] + *) + | _ -> infer_type env f, [] + in + let f' = Dedukti.apps (translate_constr info env uenv f) template_univ_parameters in + let translate_app (f', type_f) u = + debug "Type f : %a" (pp_coq_term_env env) type_f; + let _, c, d = Constr.destProd (Reduction.whd_all env type_f) in + let u' = translate_constr ~expected_type:c info env uenv u in + (Dedukti.app f' u', Vars.subst1 u d) in + fst (Array.fold_left translate_app (f', type_f) args) | Const ((kn, univ_instance) as knu) -> - let name = Cname.translate_constant info env kn in - debug "Printing constant: %s@@{%a}" name pp_coq_inst univ_instance; - if Utils.str_starts_with "Little__fix" name - then Dedukti.var (Utils.truncate name 8) - else if Utils.str_starts_with "fix_" name || - not (Encoding.is_polymorphism_on ()) - then Dedukti.var name - else if Encoding.is_polymorphism_on () && - Environ.polymorphic_pconstant knu env - then - (* FIXME: add constraints here ! *) - Tsorts.instantiate_poly_univ_constant env uenv knu (Dedukti.var name) - else Dedukti.var name + let name = Cname.translate_constant info env kn in + debug "Printing constant: %s@@{%a}" name pp_coq_inst univ_instance; + if Utils.str_starts_with "Little__fix" name + then Dedukti.var (Utils.truncate name 8) + else if Utils.str_starts_with "fix_" name || + not (Encoding.is_polymorphism_on ()) + then Dedukti.var name + else if Encoding.is_polymorphism_on () && + Environ.polymorphic_pconstant knu env + then (* FIXME: add constraints here ! *) + Tsorts.instantiate_poly_univ_constant env uenv knu (Dedukti.var name) + else Dedukti.var name | Ind (ind, univ_instance) -> - let name = Cname.translate_inductive info env ind in - debug "Printing inductive: %s@@{%a}" name pp_coq_inst univ_instance; - (* FIXME: add constraints here ! *) - Tsorts.instantiate_poly_ind_univ_params env uenv ind univ_instance - (Tsorts.instantiate_template_ind_univ_params env uenv ind univ_instance - (Dedukti.var name)) + let name = Cname.translate_inductive info env ind in + debug "Printing inductive: %s@@{%a}" name pp_coq_inst univ_instance; + (* FIXME: add constraints here ! *) + Tsorts.instantiate_poly_ind_univ_params env uenv ind univ_instance + (Tsorts.instantiate_template_ind_univ_params env uenv ind univ_instance + (Dedukti.var name)) | Construct (kn, univ_instance) -> - let name = Cname.translate_constructor info env kn in - debug "Printing constructor: %s@@{%a}" name pp_coq_inst univ_instance; - let ind = Names.inductive_of_constructor kn in - Tsorts.instantiate_poly_ind_univ_params env uenv ind univ_instance - ( if Tsorts.template_constructor_upoly () - then - (* FIXME: add constraints here ! *) - Tsorts.instantiate_template_ind_univ_params env uenv ind univ_instance - (Dedukti.var name) - else Dedukti.var name ) + let name = Cname.translate_constructor info env kn in + debug "Printing constructor: %s@@{%a}" name pp_coq_inst univ_instance; + let ind = Names.inductive_of_constructor kn in + Tsorts.instantiate_poly_ind_univ_params env uenv ind univ_instance + ( if Tsorts.template_constructor_upoly () + then + (* FIXME: add constraints here ! *) + Tsorts.instantiate_template_ind_univ_params env uenv ind univ_instance + (Dedukti.var name) + else Dedukti.var name ) | Fix (((rec_indices, i), ((names, types, bodies) as rec_declaration)) as fp) -> - if Encoding.is_fixpoint_inlined () - then translate_fixpoint info env uenv fp (Array.map (infer_type env) types) - else - begin - let n = Array.length names in - debug "Translating %i fixpoints:" n; - for i = 0 to n - 1 do - debug "%i -> %a : %a" i - (pp_coq_binder pp_coq_name) names.(i) - pp_coq_term types.(i); - debug "body: %a" pp_coq_term bodies.(i); - done; - (* TODO: not the whole environment should be added here, only the relevant part - i.e. variables that occur in the body of the fixpoint *) - let env, fix_declarations = - let fsig = fixpoint_signature env rec_declaration in - try Hashtbl.find fixpoint_table fsig - with Not_found -> - let res = lift_fix info env uenv names types bodies rec_indices in - Hashtbl.add fixpoint_table fsig res; - res - in - let new_env = - Array.fold_left - (fun env declaration -> Environ.push_rel declaration env) - env fix_declarations in - translate_constr info new_env uenv (Constr.mkRel (n - i)) - end + if Encoding.is_fixpoint_inlined () + then translate_fixpoint info env uenv fp (Array.map (infer_type env) types) + else + begin + let n = Array.length names in + debug "Translating %i fixpoints:" n; + for i = 0 to n - 1 do + debug "%i -> %a : %a" i + (pp_coq_binder pp_coq_name) names.(i) + pp_coq_term types.(i); + debug "body: %a" pp_coq_term bodies.(i); + done; + (* TODO: not the whole environment should be added here, + only the relevant part + i.e. variables that occur in the body of the fixpoint *) + let env, fix_declarations = + let fsig = fixpoint_signature env rec_declaration in + try Hashtbl.find fixpoint_table fsig + with Not_found -> + let res = lift_fix info env uenv names types bodies rec_indices in + Hashtbl.add fixpoint_table fsig res; + res + in + let new_env = + Array.fold_left + (fun env declaration -> Environ.push_rel declaration env) + env fix_declarations in + translate_constr info new_env uenv (Constr.mkRel (n - i)) + end | Case(case_info, return_type, matched, branches) -> - let match_function_name = Cname.translate_match_function info env case_info.ci_ind in - let mind_body, ind_body = Inductive.lookup_mind_specif env case_info.ci_ind in - let n_params = mind_body.Declarations.mind_nparams in - let n_reals = ind_body.Declarations.mind_nrealargs in - let pind, ind_args = Inductive.find_rectype env (infer_type env matched) in - (* - let arity = Inductive.type_of_inductive env ( (mind_body, ind_body), snd pind) in - *) - let params, reals = Utils.list_chop n_params ind_args in - (* Probably put that back - let params = List.map (Reduction.whd_all env) params in - *) - debug "Template universe params: %a" (pp_list ", " pp_coq_term) params; - (* FIXME: This is not correct ! - We do not provide universe level allowing substitution - of universe polymorphic destructions. *) - let arity, univ_params' = - infer_dest_applied info env uenv pind (Array.of_list params) - in - let univ_poly_levels = - if Encoding.is_polymorphism_on () - then - Tsorts.get_poly_univ_params uenv - (Declareops.inductive_polymorphic_context mind_body) (snd pind) - else [] in - let context, end_type = Term.decompose_lam_n_assum (n_reals + 1) return_type in - let return_sort = infer_sort (Environ.push_rel_context context env) end_type in - (* Translate params using expected types to make sure we use proper casts. *) - let translate_param (params', a) param = - let _, c, d = Constr.destProd (Reduction.whd_all env a) in - let param' = translate_constr ~expected_type:c info env uenv param in - (param' :: params', Vars.subst1 param d) in - let match_function' = Dedukti.var match_function_name in - let return_sort' = Tsorts.translate_sort uenv return_sort in - let return_sort' = T.coq_universe return_sort' in - let params' = List.rev (fst (List.fold_left translate_param ([], arity) params)) in - debug "params': %a" (pp_list ", " Dedukti.pp_term) params'; - let return_type' = translate_constr info env uenv return_type in - let branches' = Array.to_list (Array.map (translate_constr info env uenv) branches) in - let reals' = List.map (translate_constr info env uenv) reals in - let matched' = translate_constr info env uenv matched in - Dedukti.apps match_function' - (univ_params' @ univ_poly_levels @ return_sort' :: params' @ return_type' :: branches' @ reals' @ [matched']) + let match_function_name = Cname.translate_match_function info env case_info.ci_ind in + let mind_body, ind_body = Inductive.lookup_mind_specif env case_info.ci_ind in + let n_params = mind_body.Declarations.mind_nparams in + let n_reals = ind_body.Declarations.mind_nrealargs in + let pind, ind_args = Inductive.find_rectype env (infer_type env matched) in + (* + let arity = Inductive.type_of_inductive env + ( (mind_body, ind_body), snd pind) in + *) + let params, reals = Utils.list_chop n_params ind_args in + (* Probably put that back + let params = List.map (Reduction.whd_all env) params in + *) + debug "Template universe params: %a" (pp_list ", " pp_coq_term) params; + (* FIXME: This is not correct ! + We do not provide universe level allowing substitution + of universe polymorphic destructions. *) + let arity, univ_params' = + infer_dest_applied info env uenv pind (Array.of_list params) + in + let univ_poly_levels = + if Encoding.is_polymorphism_on () + then + Tsorts.get_poly_univ_params uenv + (Declareops.inductive_polymorphic_context mind_body) (snd pind) + else [] in + let context, end_type = Term.decompose_lam_n_assum (n_reals + 1) return_type in + let return_sort = infer_sort (Environ.push_rel_context context env) end_type in + (* Translate params using expected types to make sure we use proper casts. *) + let translate_param (params', a) param = + let _, c, d = Constr.destProd (Reduction.whd_all env a) in + let param' = translate_constr ~expected_type:c info env uenv param in + (param' :: params', Vars.subst1 param d) in + let match_function' = Dedukti.var match_function_name in + let return_sort' = Tsorts.translate_sort uenv return_sort in + let return_sort' = T.coq_universe return_sort' in + let params' = List.rev (fst (List.fold_left translate_param ([], arity) params)) in + debug "params': %a" (pp_list ", " Dedukti.pp_term) params'; + let return_type' = translate_constr info env uenv return_type in + let branches' = Array.to_list (Array.map (translate_constr info env uenv) branches) in + let reals' = List.map (translate_constr info env uenv) reals in + let matched' = translate_constr info env uenv matched in + Dedukti.apps match_function' + (univ_params' @ univ_poly_levels @ return_sort' :: params' @ return_type' :: branches' @ reals' @ [matched']) (* Not yet supported cases: *) | Proj (p,t) -> @@ -703,8 +698,8 @@ and translate_fixpoint info env uenv (fp:(Constr.constr,Constr.types) Constr.pfi -and lift_let info env uenv x u a = - let name = Context.binder_name x in +and lift_let info env uenv binda u a = + let name = Context.binder_name binda in let y = Cname.fresh_of_name ~global:true ~prefix:"let" ~default:"_" info env name in let yconstant = make_const info.module_path y in let y' = Cname.translate_constant info env yconstant in @@ -722,7 +717,8 @@ and lift_let info env uenv x u a = let inst = Univ.UContext.instance (Univ.AUContext.repr uenv.poly_ctxt) in let yconstr = apply_rel_context (Constr.mkConstU (yconstant,inst)) rel_context in let env = push_const_decl uenv env (yconstant, Some(u_closed), a_closed) in - let new_env = Environ.push_rel (Context.Rel.Declaration.LocalDef(x, yconstr, a)) env in + let def = Context.Rel.Declaration.LocalDef(binda, yconstr, a) in + let new_env = Environ.push_rel def env in new_env and lift_fix info env uenv names types bodies rec_indices = From dd66e79671eabf8d088f9ca0ec7c42d034fcf760 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Thu, 6 Feb 2020 15:58:46 +0100 Subject: [PATCH 3/7] Removed comments. --- Makefile | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Makefile b/Makefile index 2eb76a4..d905391 100644 --- a/Makefile +++ b/Makefile @@ -8,8 +8,6 @@ DKCHECK ?= dkcheck DKDEP ?= dkdep VERBOSE ?= -CAMLFLAGS="-bin-annot -annot" - RUNDIR=run COQ_VERSION := $(shell $(COQTOP) -print-version) @@ -140,10 +138,6 @@ fullclean: clean rm src/*.cmti rm src/*.annot -# CoqMakefile: Make -# $(COQ_MAKEFILE) -f Make -o CoqMakefile -# echo "COQMF_CAMLFLAGS+=-annot -bin-annot -g" >> CoqMakefile.conf - .coqrc: plugin echo "Add ML Path \"$(shell pwd)/src\"." > .coqrc From f36a6ff643e74639a99a7eb2ab506f2ebd94ee03 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Tue, 11 Feb 2020 12:24:26 +0100 Subject: [PATCH 4/7] Fixed tests. --- run/upoly_logipedia/import.v | 10 ++++++---- run/upoly_logipedia/main.v | 6 ++++-- src/modules.ml | 14 ++++++++------ 3 files changed, 18 insertions(+), 12 deletions(-) diff --git a/run/upoly_logipedia/import.v b/run/upoly_logipedia/import.v index 663cdfc..60627d8 100644 --- a/run/upoly_logipedia/import.v +++ b/run/upoly_logipedia/import.v @@ -14,23 +14,25 @@ Require Import Coq.Init.Wf Coq.Init.Tactics Coq.Init.Tauto - Coq.Bool.Bool Coq.Bool.BoolEq Coq.Bool.DecBool - Coq.Bool.IfProp (* + Coq.Bool.IfProp Coq.Bool.Sumbool +(* Coq.Bool.Zerob Coq.Bool.Bvector (* Requires Coq.PArith.BinPos which is bugged *) *) - Coq.Logic.ProofIrrelevanceFacts (* + Coq.Logic.ProofIrrelevanceFacts Coq.Logic.Decidable +(* Coq.Logic.Hurkens (* Bug to fix... *) *) + +(* Coq.Arith.Arith_base - (* Coq.Lists.List (* Requires Coq.PArith.BinPos which is bugged *) *) . diff --git a/run/upoly_logipedia/main.v b/run/upoly_logipedia/main.v index 4a56263..bb0360c 100644 --- a/run/upoly_logipedia/main.v +++ b/run/upoly_logipedia/main.v @@ -4,13 +4,15 @@ Load config. Dedukti Set Param "simpl_letins" "false". Dedukti Enable Failproofmode. -Dedukti Enable Verbose. +(* Set Printing All. Set Printing Universes. Dedukti Enable Debug. Dedukti Set Debug "debug.out". -Dedukti Add Debug "Coq.PArith.BinPos". +Dedukti Add Debug "Coq.Classes.CMorphisms". +Dedukti Enable Verbose. + *) Require Import import. Dedukti Export All. diff --git a/src/modules.ml b/src/modules.ml index 685697b..689aafe 100644 --- a/src/modules.ml +++ b/src/modules.ml @@ -6,8 +6,14 @@ open Info let fail_on_issue = ref true -let enable_failproofmode () = message "Failproof mode enabled." ; fail_on_issue := false -let disable_failproofmode () = message "Failproof mode disabled."; fail_on_issue := true + +let enable_failproofmode () = + message "Failproof mode enabled."; + fail_on_issue := false + +let disable_failproofmode () = + message "Failproof mode disabled."; + fail_on_issue := true let symb_filter = ref [] let filter_out symb = symb_filter := symb :: !symb_filter @@ -231,9 +237,7 @@ and translate_structure_field_body info env resolver (label, sfb) = if not_filtered full_name then begin - (* try - *) verbose "-> %s" full_name; let kername = Names.KerName.make info.module_path label in match sfb with @@ -247,12 +251,10 @@ and translate_structure_field_body info env resolver (label, sfb) = ) info env (isalias resolver kername) label mib; | SFBmodule mb -> translate_module_body (Info.update info label) env mb | SFBmodtype _ -> () - (* with e -> if !fail_on_issue then (Info.close info; raise e) else verbose "[Error] On symbol %s: %s" full_name (Printexc.to_string e) - *) end else begin From e2df3a1b930e2b1f82d0543dcab11a575f3d127e Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Wed, 12 Feb 2020 11:50:44 +0100 Subject: [PATCH 5/7] Fixed .travis --- .travis.yml | 8 ++++---- run/upoly_logipedia/import.v | 3 ++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/.travis.yml b/.travis.yml index 239037a..f552574 100644 --- a/.travis.yml +++ b/.travis.yml @@ -15,8 +15,8 @@ cache: env: global: - OPAMJOBS="2" - - OPAMYES="true" - - OPAMVERBOSE="true" + - OPAMYES=1 + - OPAMVERBOSE=1 - OCAML_VERSION=4.09.0 before_install: @@ -26,8 +26,8 @@ before_install: # Initialize the switch. - opam init -a --disable-sandboxing --compiler="$OCAML_VERSION" - opam update - - opam switch "$OCAML_VERSION" - - eval $(opam env) + - opam switch ${OCAML_VERSION} || opam switch create ${OCAML_VERSION} + - eval `opam config env` - opam pin add dedukti https://github.com/Deducteam/Dedukti.git#acu-state - opam install dedukti - opam pin add --no-action coqine . diff --git a/run/upoly_logipedia/import.v b/run/upoly_logipedia/import.v index 60627d8..dbeaa5f 100644 --- a/run/upoly_logipedia/import.v +++ b/run/upoly_logipedia/import.v @@ -1,6 +1,7 @@ (* Require Import Coq.PArith.BinPos. -**) +Require Import Coq.Classes.CMorphisms. +*) Require Import Coq.Init.Notations From f612717e307c388a800618a239c92340368a171d Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Wed, 13 May 2020 10:32:58 +0200 Subject: [PATCH 6/7] WIP --- Makefile | 14 +++++++++++--- run/main/Test/Test.v | 7 ++++++- run/main/main_debug.v | 2 +- run/main/main_poly.v | 2 +- run/main/main_test.v | 2 +- run/upoly_logipedia/import.v | 8 +++++--- run/upoly_logipedia/main.v | 10 +++++++--- src/commands.mlg | 7 ++++++- src/debug.ml | 4 ++++ src/debug.mli | 7 +++++++ src/info.ml | 11 ++++++++++- src/modules.ml | 4 +++- src/terms.ml | 4 +--- 13 files changed, 63 insertions(+), 19 deletions(-) diff --git a/Makefile b/Makefile index d905391..a923061 100644 --- a/Makefile +++ b/Makefile @@ -134,9 +134,17 @@ clean: rm -f summary.csv fullclean: clean - rm src/*.cmt - rm src/*.cmti - rm src/*.annot + rm -f src/*.annot + rm -f src/*.cmo + rm -f src/*.cma + rm -f src/*.cmi + rm -f src/*.cmt + rm -f src/*.cmti + rm -f src/*.a + rm -f src/*.o + rm -f src/*.cmx + rm -f src/*.cmxs + rm -f src/*.cmxa .coqrc: plugin echo "Add ML Path \"$(shell pwd)/src\"." > .coqrc diff --git a/run/main/Test/Test.v b/run/main/Test/Test.v index e906c08..3f36347 100644 --- a/run/main/Test/Test.v +++ b/run/main/Test/Test.v @@ -3,9 +3,14 @@ Inductive list {A:Type} : Type := | Nil : list | Cons : A -> list -> list. -Definition f : nat -> nat := +Definition g : nat -> nat := fun x => (fix aux (n:nat) : nat := 0) x. +Definition f : nat -> nat := + fix f (n:nat) {struct n} : nat := match n with 0 => 0 | S n' => S (g n') end + with g (n:nat) {struct n} : nat := n + for f. + (* Eval compute in (fun x => f x). *) diff --git a/run/main/main_debug.v b/run/main/main_debug.v index b8c121e..e9e4a4f 100644 --- a/run/main/main_debug.v +++ b/run/main/main_debug.v @@ -10,7 +10,7 @@ Dedukti Set Destination "out". Dedukti Enable Debug. Dedukti Set Debug "debug.out". -Dedukti Add Debug "Coq.Init.Logic". +Dedukti Debug Lib "Coq.Init.Logic". Require Import import_debug. diff --git a/run/main/main_poly.v b/run/main/main_poly.v index ac0f7f3..c621135 100644 --- a/run/main/main_poly.v +++ b/run/main/main_poly.v @@ -10,7 +10,7 @@ Dedukti Set Destination "out". Dedukti Enable Debug. Dedukti Set Debug "debug.out". -Dedukti Add Debug "Top.Test.Debug". +Dedukti Debug Lib "Top.Test.Debug". Dedukti Enable Verbose. diff --git a/run/main/main_test.v b/run/main/main_test.v index 9d212ac..cb10849 100644 --- a/run/main/main_test.v +++ b/run/main/main_test.v @@ -12,7 +12,7 @@ Dedukti Set Destination "out". Dedukti Enable Debug. Dedukti Set Debug "debug.out". -Dedukti Add Debug "Coq.Init.Datatype". +Dedukti Debug Lib "Coq.Init.Datatype". (* Import some modules to translate *) Require Import Test.Fixpoints. diff --git a/run/upoly_logipedia/import.v b/run/upoly_logipedia/import.v index dbeaa5f..c05ab55 100644 --- a/run/upoly_logipedia/import.v +++ b/run/upoly_logipedia/import.v @@ -4,6 +4,7 @@ Require Import Coq.Classes.CMorphisms. *) Require Import +(* Coq.Init.Notations Coq.Init.Logic Coq.Init.Logic_Type @@ -20,16 +21,17 @@ Require Import Coq.Bool.DecBool Coq.Bool.IfProp Coq.Bool.Sumbool +*) + (* Coq.Bool.Zerob Coq.Bool.Bvector (* Requires Coq.PArith.BinPos which is bugged *) *) - Coq.Logic.ProofIrrelevanceFacts - Coq.Logic.Decidable (* + Coq.Logic.ProofIrrelevanceFacts + Coq.Logic.Decidable *) Coq.Logic.Hurkens (* Bug to fix... *) -*) (* Coq.Arith.Arith_base diff --git a/run/upoly_logipedia/main.v b/run/upoly_logipedia/main.v index bb0360c..7cd52a5 100644 --- a/run/upoly_logipedia/main.v +++ b/run/upoly_logipedia/main.v @@ -3,16 +3,20 @@ Dedukti Set Destination "out". Load config. Dedukti Set Param "simpl_letins" "false". +(* Dedukti Enable Failproofmode. + *) -(* Set Printing All. Set Printing Universes. Dedukti Enable Debug. Dedukti Set Debug "debug.out". -Dedukti Add Debug "Coq.Classes.CMorphisms". -Dedukti Enable Verbose. +Dedukti Debug Lib "Coq.Logic.Hurkens.NoRetractToImpredicativeUniverse". +(* +Dedukti Debug Symbol "Coq.Logic.Hurkens.NoRetractToModalProposition.paradox". *) +Dedukti Enable Verbose. + Require Import import. Dedukti Export All. diff --git a/src/commands.mlg b/src/commands.mlg index 52cc6d2..2c7310b 100644 --- a/src/commands.mlg +++ b/src/commands.mlg @@ -61,10 +61,15 @@ VERNAC COMMAND EXTEND DeduktiSetDebug CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND DeduktiAddDebug CLASSIFIED AS QUERY -| [ "Dedukti" "Add" "Debug" string(lib) ] -> +| [ "Dedukti" "Debug" "Lib" string(lib) ] -> { Debug.add_debug_lib lib } END +VERNAC COMMAND EXTEND DeduktiAddDebug CLASSIFIED AS QUERY +| [ "Dedukti" "Debug" "Symbol" string(lib) ] -> + { Debug.add_debug_smb lib } +END + VERNAC COMMAND EXTEND DeduktiFilterSymb CLASSIFIED AS QUERY | [ "Dedukti" "Filter" "Out" string(symb) ] -> { Modules.filter_out symb } diff --git a/src/debug.ml b/src/debug.ml index 45f5b9a..ff5ed7f 100644 --- a/src/debug.ml +++ b/src/debug.ml @@ -5,6 +5,10 @@ let debug_libraries = ref [] let add_debug_lib s = debug_libraries := s :: !debug_libraries let is_debug_lib s = List.exists (fun x -> s = str x) !debug_libraries +let debug_symbols = ref [] +let add_debug_smb s = debug_symbols := s :: !debug_symbols +let is_debug_smb s = List.mem s !debug_symbols + let debug_allowed = ref false let enable_debug () = debug_allowed := true let disable_debug () = debug_allowed := false diff --git a/src/debug.mli b/src/debug.mli index b3693c3..400d75c 100644 --- a/src/debug.mli +++ b/src/debug.mli @@ -23,6 +23,13 @@ val is_debug_lib : Pp.t -> bool (** Should debug be enabled for given library ? *) +val add_debug_smb : string -> unit +(** Add symbol name to debug list *) + +val is_debug_smb : string -> bool +(** Should debug be enabled for given symbol ? *) + + val debug_start : unit -> unit (** Starts debugging *) diff --git a/src/info.ml b/src/info.ml index 8283f74..1665c08 100644 --- a/src/info.ml +++ b/src/info.ml @@ -45,7 +45,16 @@ let fetch_constraint uenv cstr = let fetch_higher_sorts uenv u = let assoc acc ((i,c,j),(b,_,_)) = - if compare i u = 0 then (c,j,b)::acc else acc + match c with + | AcyclicGraph.Eq -> + if compare i u = 0 + then (c,j,b)::acc + else if compare j u = 0 + then (c,i,b)::acc + else acc + | _ -> + if compare i u = 0 + then (c,j,b)::acc else acc (* FIXME: Equality constraints are not handled correctly here. - They should be considered both way - We should also prevent loops somehow *) diff --git a/src/modules.ml b/src/modules.ml index 689aafe..04be096 100644 --- a/src/modules.ml +++ b/src/modules.ml @@ -230,6 +230,7 @@ and translate_module_signature info env resolver = function and translate_structure_field_body info env resolver (label, sfb) = let full_name = (Names.ModPath.to_string info.module_path) ^ "." ^ (Names.Label.to_string label) in + if Debug.is_debug_smb full_name then debug_start (); debug ""; debug "---------------------------------------------"; debug " Structure field body: %s" full_name; @@ -260,4 +261,5 @@ and translate_structure_field_body info env resolver (label, sfb) = begin debug "Filtered out"; verbose "-> %s (ignored)" full_name - end + end; + if Debug.is_debug_smb full_name then debug_stop (); diff --git a/src/terms.ml b/src/terms.ml index 2971f59..59504c6 100644 --- a/src/terms.ml +++ b/src/terms.ml @@ -302,6 +302,7 @@ let infer_dest_applied info env uenv (ind,u) args = else arity, [] let rec translate_constr ?expected_type info env uenv t = + debug "Translating term %a" (pp_coq_term_env env) t; (* Check if the expected type coincides, otherwise make an explicit cast. *) let t = match expected_type with @@ -576,10 +577,7 @@ and translate_cast info uenv t' enva a envb b = with Reduction.NotArity -> Tsorts.enforce_eq_types Univ.Constraint.empty [(a,b)] in - debug "Constraints: %a" pp_coq_Constraint constraints; let var_cstr = Tsorts.translate_constraints_as_conjunction uenv constraints in - debug "Found constraints %a" (pp_list ", " Dedukti.pp_term) (List.map fst var_cstr); - debug "Found constraints %a" (pp_list ", " Dedukti.pp_term) (List.map snd var_cstr); T.coq_cast s1' s2' a' b' var_cstr t' else if Term.isArity a && Term.isArity b From 91bbdfa6d0fa02d2741b3b686f17a632c3b41219 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Tue, 28 Jul 2020 08:40:00 +0200 Subject: [PATCH 7/7] Make test working --- run/main/Test/Fixpoints.v | 37 ++++++++++++++++++++++++++++++++++++ run/upoly_logipedia/import.v | 14 +++++--------- run/upoly_logipedia/main.v | 28 +++++++++++++++++++++------ 3 files changed, 64 insertions(+), 15 deletions(-) diff --git a/run/main/Test/Fixpoints.v b/run/main/Test/Fixpoints.v index d5f72a2..c68bba2 100644 --- a/run/main/Test/Fixpoints.v +++ b/run/main/Test/Fixpoints.v @@ -1,13 +1,39 @@ + Inductive nat := | o : nat | s : nat -> nat. +Definition plus_nat : nat -> nat -> nat := + fun n => + ( + fix aux (m:nat) {struct m} : nat + := match m with + | o => n + | s m' => s (aux m') end + ). + +Definition even : nat -> bool := + (fix even' (n:nat) : bool + := + (match n with + o => true + | s n' => odd' n' + end) + with odd' (n:nat) : bool + := + (match n with + o => false + | s n' => even' n' + end) + for even'). + Fixpoint id x := match x with | o => o | s x => s (id x) end. + Fixpoint id1 a b n := match n with | o => a @@ -32,6 +58,17 @@ Fixpoint f x := end) x. +Fixpoint f' x := + match x with + | o => o + | s x1 => g' x1 + end +with g' y := + match y with + | o => o + | s y1 => f' y1 + end. + Inductive nat' : Type := | Z' : nat' diff --git a/run/upoly_logipedia/import.v b/run/upoly_logipedia/import.v index c05ab55..fe94885 100644 --- a/run/upoly_logipedia/import.v +++ b/run/upoly_logipedia/import.v @@ -1,10 +1,4 @@ -(* -Require Import Coq.PArith.BinPos. -Require Import Coq.Classes.CMorphisms. -*) - Require Import -(* Coq.Init.Notations Coq.Init.Logic Coq.Init.Logic_Type @@ -21,18 +15,20 @@ Require Import Coq.Bool.DecBool Coq.Bool.IfProp Coq.Bool.Sumbool -*) (* + Coq.PArith.BinPos. + Coq.Classes.CMorphisms. + Coq.Bool.Zerob Coq.Bool.Bvector (* Requires Coq.PArith.BinPos which is bugged *) *) (* Coq.Logic.ProofIrrelevanceFacts - Coq.Logic.Decidable *) + Coq.Logic.Decidable Coq.Logic.Hurkens (* Bug to fix... *) - +*) (* Coq.Arith.Arith_base diff --git a/run/upoly_logipedia/main.v b/run/upoly_logipedia/main.v index 7cd52a5..a3c038d 100644 --- a/run/upoly_logipedia/main.v +++ b/run/upoly_logipedia/main.v @@ -3,20 +3,36 @@ Dedukti Set Destination "out". Load config. Dedukti Set Param "simpl_letins" "false". +Require Import import. + +Dedukti Export All. + (* Dedukti Enable Failproofmode. - *) Set Printing All. Set Printing Universes. + Dedukti Enable Debug. Dedukti Set Debug "debug.out". Dedukti Debug Lib "Coq.Logic.Hurkens.NoRetractToImpredicativeUniverse". -(* Dedukti Debug Symbol "Coq.Logic.Hurkens.NoRetractToModalProposition.paradox". - *) - Dedukti Enable Verbose. -Require Import import. -Dedukti Export All. +Require Import + Coq.PArith.BinPos. + Coq.Classes.CMorphisms. + + Coq.Bool.Zerob + Coq.Bool.Bvector (* Requires Coq.PArith.BinPos which is bugged *) + + Coq.Logic.ProofIrrelevanceFacts + Coq.Logic.Decidable + Coq.Logic.Hurkens (* Bug to fix... *) + Coq.Arith.Arith_base + + Coq.Lists.List (* Requires Coq.PArith.BinPos which is bugged *) +. + +Dedukti Export Library Coq.Logic.Hurkens. +*)