diff --git a/src/reify.ml4 b/src/reify.ml4 index cdbf73e09..f5c583b91 100644 --- a/src/reify.ml4 +++ b/src/reify.ml4 @@ -90,6 +90,29 @@ module Mindset = Names.Mindset type ('a,'b) sum = Left of 'a | Right of 'b +type ('term, 'name, 'nat) adef = { adname : 'name; adtype : 'term; adbody : 'term; rarg : 'nat } + +type ('term, 'name, 'nat) amfixpoint = ('term, 'name, 'nat) adef list + +type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive, 'universe_instance, 'projection) structure_of_term = + | ACoq_tRel of 'nat + | ACoq_tVar of 'ident + | ACoq_tMeta of 'nat + | ACoq_tEvar of 'nat * 'term list + | ACoq_tSort of 'quoted_sort + | ACoq_tCast of 'term * 'cast_kind * 'term + | ACoq_tProd of 'name * 'term * 'term + | ACoq_tLambda of 'name * 'term * 'term + | ACoq_tLetIn of 'name * 'term * 'term * 'term + | ACoq_tApp of 'term * 'term list + | ACoq_tConst of 'kername * 'universe_instance + | ACoq_tInd of 'inductive * 'universe_instance + | ACoq_tConstruct of 'inductive * 'nat * 'universe_instance + | ACoq_tCase of ('inductive * 'nat) * 'term * 'term * ('nat * 'term) list + | ACoq_tProj of 'projection * 'term + | ACoq_tFix of ('term, 'name, 'nat) amfixpoint * 'nat + | ACoq_tCoFix of ('term, 'name, 'nat) amfixpoint * 'nat + module type Quoter = sig type t @@ -108,10 +131,11 @@ module type Quoter = sig type quoted_univ_instance type quoted_univ_constraints type quoted_univ_context + type quoted_inductive_universes type quoted_mind_params type quoted_ind_entry = quoted_ident * t * quoted_bool * quoted_ident list * t list - type quoted_definition_entry = t * t option + type quoted_definition_entry = t * t option * quoted_univ_context type quoted_mind_entry type quoted_mind_finiteness type quoted_entry @@ -119,6 +143,8 @@ module type Quoter = sig type quoted_sort_family open Names + + val quote_ident : Id.t -> quoted_ident val quote_name : Name.t -> quoted_name @@ -135,14 +161,16 @@ module type Quoter = sig val quote_univ_constraints : Univ.Constraint.t -> quoted_univ_constraints val quote_univ_context : Univ.UContext.t -> quoted_univ_context val quote_abstract_univ_context : Univ.AUContext.t -> quoted_univ_context + val quote_inductive_universes : inductive_universes -> quoted_inductive_universes - (* val quote_mind_params : (quoted_ident * (t,t) sum) list -> quoted_mind_params *) - (* val quote_mind_finiteness : Decl_kinds.recursivity_kind -> quoted_mind_finiteness *) - (* val quote_mutual_inductive_entry : *) - (* quoted_mind_finiteness * quoted_mind_params * quoted_ind_entry list * quoted_bool -> *) - (* quoted_mind_entry *) + val quote_mind_params : (quoted_ident * (t,t) sum) list -> quoted_mind_params + val quote_mind_finiteness : Decl_kinds.recursivity_kind -> quoted_mind_finiteness + val quote_mutual_inductive_entry : + quoted_mind_finiteness * quoted_mind_params * quoted_ind_entry list * + quoted_inductive_universes -> + quoted_mind_entry - (* val quote_entry : (quoted_definition_entry, quoted_mind_entry) sum option -> quoted_entry *) + val quote_entry : (quoted_definition_entry, quoted_mind_entry) sum option -> quoted_entry val quote_proj : quoted_inductive -> quoted_int -> quoted_int -> quoted_proj val mkName : quoted_ident -> quoted_name @@ -180,8 +208,34 @@ module type Quoter = sig val mkExt : quoted_decl -> quoted_program -> quoted_program val mkIn : t -> quoted_program + + val unquote_ident : quoted_ident -> Id.t + val unquote_name : quoted_name -> Name.t + val unquote_int : quoted_int -> int + val unquote_bool : quoted_bool -> bool + (* val unquote_sort : quoted_sort -> Sorts.t + val unquote_sort_family : quoted_sort_family -> Sorts.family *) + val unquote_cast_kind : quoted_cast_kind -> Constr.cast_kind + val unquote_kn : quoted_kernel_name -> Libnames.qualid + val unquote_inductive : quoted_inductive -> Names.inductive + (* val unquote_univ_instance : quoted_univ_instance -> Univ.Instance.t *) + val unquote_proj : quoted_proj -> (quoted_inductive * quoted_int * quoted_int) + val unquote_universe : Evd.evar_map -> quoted_sort -> Evd.evar_map * Univ.Universe.t + val print_term : t -> Pp.std_ppcmds + (* val representsIndConstuctor : quoted_inductive -> Term.constr -> bool *) + val inspectTerm : t -> (t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_univ_instance, quoted_proj) structure_of_term end +let reduce_hnf env evm (trm : Term.constr) = + let trm = Tacred.hnf_constr env evm (EConstr.of_constr trm) in + (evm, EConstr.to_constr evm trm) + +let reduce_all env evm ?(red=Genredexpr.Cbv Redops.all_flags) trm = + let red, _ = Redexpr.reduction_of_red_expr env red in + let evm, red = red env evm (EConstr.of_constr trm) in + (evm, EConstr.to_constr evm red) + + (** The reifier to Coq values *) module TemplateCoqQuoter = struct @@ -200,6 +254,7 @@ struct type quoted_univ_constraints = Term.constr (* of type univ.constraints *) type quoted_univ_instance = Term.constr (* of type univ.universe_instance *) type quoted_univ_context = Term.constr (* of type univ.universe_context *) + type quoted_inductive_universes = Term.constr (* of type univ.universe_context *) type quoted_proj = Term.constr (* of type Ast.projection *) type quoted_sort_family = Term.constr (* of type Ast.sort_family *) @@ -211,7 +266,7 @@ struct type quoted_mind_entry = Term.constr (* of type Ast.mutual_inductive_entry *) type quoted_mind_finiteness = Term.constr (* of type Ast.mutual_inductive_entry *) - type quoted_definition_entry = t * t option + type quoted_definition_entry = t * t option * quoted_univ_context type quoted_entry = Term.constr (* of type option (constant_entry + mutual_inductive_entry) *) type quoted_global_reference = Term.constr (* of type Ast.global_reference *) type quoted_reduction_strategy = Term.constr (* of type Ast.reductionStrategy *) @@ -243,11 +298,11 @@ struct let c_nil = resolve_symbol pkg_datatypes "nil" let c_cons = resolve_symbol pkg_datatypes "cons" let prod_type = resolve_symbol pkg_datatypes "prod" - (* let sum_type = resolve_symbol pkg_datatypes "sum" - * let option_type = resolve_symbol pkg_datatypes "option" *) + let sum_type = resolve_symbol pkg_datatypes "sum" + let option_type = resolve_symbol pkg_datatypes "option" let bool_type = resolve_symbol pkg_datatypes "bool" - (* let cInl = resolve_symbol pkg_datatypes "inl" - * let cInr = resolve_symbol pkg_datatypes "inr" *) + let cInl = resolve_symbol pkg_datatypes "inl" + let cInr = resolve_symbol pkg_datatypes "inr" let prod a b = Term.mkApp (prod_type, [| a ; b |]) let c_pair = resolve_symbol pkg_datatypes "pair" @@ -284,8 +339,8 @@ struct let tunivLt = resolve_symbol pkg_univ "Lt" let tunivEq = resolve_symbol pkg_univ "Eq" (* let tunivcontext = resolve_symbol pkg_univ "universe_context" *) - let tMonomorphic_ctx = resolve_symbol pkg_univ "Monomorphic_ctx" - let tPolymorphic_ctx = resolve_symbol pkg_univ "Polymorphic_ctx" + let cMonomorphic_ctx = resolve_symbol pkg_univ "Monomorphic_ctx" + let cPolymorphic_ctx = resolve_symbol pkg_univ "Polymorphic_ctx" let tUContextmake = resolve_symbol (ext_pkg_univ "UContext") "make" (* let tConstraintempty = resolve_symbol (ext_pkg_univ "Constraint") "empty" *) let tConstraintempty = Universes.constr_of_global (Coqlib.find_reference "template coq bug" (ext_pkg_univ "Constraint") "empty") @@ -295,7 +350,7 @@ struct let tadd_global_constraints = resolve_symbol pkg_ugraph "add_global_constraints" let (tdef,tmkdef) = (r_reify "def", r_reify "mkdef") - let (tLocalDef,tLocalAssum,_tlocal_entry) = (r_reify "LocalDef", r_reify "LocalAssum", r_reify "local_entry") + let (tLocalDef,tLocalAssum,tlocal_entry) = (r_reify "LocalDef", r_reify "LocalAssum", r_reify "local_entry") let (cFinite,cCoFinite,cBiFinite) = (r_reify "Finite", r_reify "CoFinite", r_reify "BiFinite") let (pConstr,pType,pAxiom,pIn) = @@ -304,11 +359,11 @@ struct let tmkinductive_body = r_reify "mkinductive_body" let tBuild_minductive_decl = r_reify "Build_minductive_decl" - let _tMutual_inductive_entry = r_reify "mutual_inductive_entry" - let _tOne_inductive_entry = r_reify "one_inductive_entry" - let _tBuild_mutual_inductive_entry = r_reify "Build_mutual_inductive_entry" - let _tBuild_one_inductive_entry = r_reify "Build_one_inductive_entry" - let _tConstant_entry = r_reify "constant_entry" + let tMutual_inductive_entry = r_reify "mutual_inductive_entry" + let tOne_inductive_entry = r_reify "one_inductive_entry" + let tBuild_mutual_inductive_entry = r_reify "Build_mutual_inductive_entry" + let tBuild_one_inductive_entry = r_reify "Build_one_inductive_entry" + let tConstant_entry = r_reify "constant_entry" let cParameterEntry = r_reify "ParameterEntry" let cDefinitionEntry = r_reify "DefinitionEntry" let cParameter_entry = r_reify "Build_parameter_entry" @@ -455,19 +510,29 @@ struct let quote_univ_context uctx = let inst = Univ.UContext.instance uctx in let const = Univ.UContext.constraints uctx in - Term.mkApp (tMonomorphic_ctx, [| quote_ucontext inst const |]) + Term.mkApp (cMonomorphic_ctx, [| quote_ucontext inst const |]) - let quote_abstract_univ_context uctx = - let uctx = Univ.AUContext.repr uctx in + let quote_abstract_univ_context_aux uctx = let inst = Univ.UContext.instance uctx in let const = Univ.UContext.constraints uctx in - Term.mkApp (tPolymorphic_ctx, [| quote_ucontext inst const |]) + Term.mkApp (cPolymorphic_ctx, [| quote_ucontext inst const |]) + + let quote_abstract_univ_context uctx = + let uctx = Univ.AUContext.repr uctx in + quote_abstract_univ_context_aux uctx + + let quote_inductive_universes uctx = + match uctx with + | Monomorphic_ind_entry uctx -> quote_univ_context uctx + | Polymorphic_ind_entry uctx -> quote_abstract_univ_context_aux uctx + | Cumulative_ind_entry info -> + quote_abstract_univ_context_aux (CumulativityInfo.univ_context info) (* FIXME lossy *) let quote_ugraph (g : UGraph.t) = let inst' = quote_univ_instance Univ.Instance.empty in let const' = quote_univ_constraints (UGraph.constraints_of_universes g) in let uctx = Term.mkApp (tUContextmake, [|inst' ; const'|]) in - Term.mkApp (tadd_global_constraints, [|Term.mkApp (tMonomorphic_ctx, [| uctx |]); tinit_graph|]) + Term.mkApp (tadd_global_constraints, [|Term.mkApp (cMonomorphic_ctx, [| uctx |]); tinit_graph|]) let quote_sort s = quote_universe (Sorts.univ_of_sort s) @@ -572,54 +637,51 @@ struct let mkExt x acc = Term.mkApp (x, [| acc |]) let mkIn t = Term.mkApp (pIn, [| t |]) - (* let quote_mind_finiteness (f: Decl_kinds.recursivity_kind) = *) - (* match f with *) - (* | Decl_kinds.Finite -> cFinite *) - (* | Decl_kinds.CoFinite -> cCoFinite *) - (* | Decl_kinds.BiFinite -> cBiFinite *) - - (* let make_one_inductive_entry (iname, arity, templatePoly, consnames, constypes) = *) - (* let consnames = to_coq_list tident consnames in *) - (* let constypes = to_coq_list tTerm constypes in *) - (* Term.mkApp (tBuild_one_inductive_entry, [| iname; arity; templatePoly; consnames; constypes |]) *) - - (* let quote_mind_params l = *) - (* let pair i l = pair tident tlocal_entry i l in *) - (* let map (id, ob) = *) - (* match ob with *) - (* | Left b -> pair id (Term.mkApp (tLocalDef,[|b|])) *) - (* | Right t -> pair id (Term.mkApp (tLocalAssum,[|t|])) *) - (* in *) - (* let the_prod = Term.mkApp (prod_type,[|tident; tlocal_entry|]) in *) - (* to_coq_list the_prod (List.map map l) *) - - (* let quote_mutual_inductive_entry (mf, mp, is, mpol) = *) - (* let is = to_coq_list tOne_inductive_entry (List.map make_one_inductive_entry is) in *) - (* let mpr = Term.mkApp (cNone, [|bool_type|]) in *) - (* let mr = Term.mkApp (cNone, [|Term.mkApp (option_type, [|tident|])|]) in *) - (* Term.mkApp (tBuild_mutual_inductive_entry, [| mr; mf; mp; is; mpol; mpr |]) *) - - - (* let quote_entry decl = *) - (* let opType = Term.mkApp(sum_type, [|tConstant_entry;tMutual_inductive_entry|]) in *) - (* let mkSome c t = Term.mkApp (cSome, [|opType; Term.mkApp (c, [|tConstant_entry;tMutual_inductive_entry; t|] )|]) in *) - (* let mkSomeDef = mkSome cInl in *) - (* let mkSomeInd = mkSome cInr in *) - (* let mkParameterEntry ty = *) - (* mkSomeDef (Term.mkApp (cParameterEntry, [| Term.mkApp (cParameter_entry, [|ty|]) |])) *) - (* in *) - (* let mkDefinitionEntry ty body = *) - (* let b = Term.mkApp (cDefinitionEntry, [| Term.mkApp (cDefinition_entry, [|ty;body|]) |]) in *) - (* mkSomeDef b *) - (* in *) - (* match decl with *) - (* | Some (Left (ty, body)) -> *) - (* (match body with *) - (* | None -> mkParameterEntry ty *) - (* | Some b -> mkDefinitionEntry ty b) *) - (* | Some (Right mind) -> *) - (* mkSomeInd mind *) - (* | None -> Constr.mkApp (cNone, [| opType |]) *) + let quote_mind_finiteness (f: Decl_kinds.recursivity_kind) = + match f with + | Decl_kinds.Finite -> cFinite + | Decl_kinds.CoFinite -> cCoFinite + | Decl_kinds.BiFinite -> cBiFinite + + let make_one_inductive_entry (iname, arity, templatePoly, consnames, constypes) = + let consnames = to_coq_list tident consnames in + let constypes = to_coq_list tTerm constypes in + Term.mkApp (tBuild_one_inductive_entry, [| iname; arity; templatePoly; consnames; constypes |]) + + let quote_mind_params l = + let pair i l = pair tident tlocal_entry i l in + let map (id, ob) = + match ob with + | Left b -> pair id (Term.mkApp (tLocalDef,[|b|])) + | Right t -> pair id (Term.mkApp (tLocalAssum,[|t|])) + in + let the_prod = Term.mkApp (prod_type,[|tident; tlocal_entry|]) in + to_coq_list the_prod (List.map map l) + + let quote_mutual_inductive_entry (mf, mp, is, mpol) = + let is = to_coq_list tOne_inductive_entry (List.map make_one_inductive_entry is) in + let mpr = Term.mkApp (cNone, [|bool_type|]) in + let mr = Term.mkApp (cNone, [|Term.mkApp (option_type, [|tident|])|]) in + Term.mkApp (tBuild_mutual_inductive_entry, [| mr; mf; mp; is; mpol; mpr |]) + + + let quote_constant_entry (ty, body, ctx) = + match body with + | None -> + Term.mkApp (cParameterEntry, [| Term.mkApp (cParameter_entry, [|ty; ctx|]) |]) + | Some body -> + Term.mkApp (cDefinitionEntry, + [| Term.mkApp (cDefinition_entry, [|ty;body;ctx;tfalse (*FIXME*)|]) |]) + + let quote_entry decl = + let opType = Term.mkApp(sum_type, [|tConstant_entry;tMutual_inductive_entry|]) in + let mkSome c t = Term.mkApp (cSome, [|opType; Term.mkApp (c, [|tConstant_entry;tMutual_inductive_entry; t|] )|]) in + let mkSomeDef = mkSome cInl in + let mkSomeInd = mkSome cInr in + match decl with + | Some (Left centry) -> mkSomeDef (quote_constant_entry centry) + | Some (Right mind) -> mkSomeInd mind + | None -> Constr.mkApp (cNone, [| opType |]) let quote_global_reference : Globnames.global_reference -> quoted_global_reference = function @@ -637,7 +699,305 @@ struct let k = (quote_int (k - 1)) in Term.mkApp (tConstructRef, [|quote_inductive (kn ,n); k|]) -end + let rec app_full trm acc = + match Term.kind_of_term trm with + Term.App (f, xs) -> app_full f (Array.to_list xs @ acc) + | _ -> (trm, acc) + + let print_term (u: t) : Pp.std_ppcmds = Printer.pr_constr u + + let from_coq_pair trm = + let (h,args) = app_full trm [] in + if Term.eq_constr h c_pair then + match args with + _ :: _ :: x :: y :: [] -> (x, y) + | _ -> bad_term trm + else + not_supported_verb trm "from_coq_pair" + + + let rec from_coq_list trm = + let (h,args) = app_full trm [] in + if Term.eq_constr h c_nil then [] + else if Term.eq_constr h c_cons then + match args with + _ :: x :: xs :: _ -> x :: from_coq_list xs + | _ -> bad_term trm + else + not_supported_verb trm "from_coq_list" + + let inspectTerm (t:Term.constr) : (Term.constr, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_univ_instance, quoted_proj) structure_of_term = + let (h,args) = app_full t [] in + if Term.eq_constr h tRel then + match args with + x :: _ -> ACoq_tRel x + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tVar then + match args with + x :: _ -> ACoq_tVar x + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tMeta then + match args with + x :: _ -> ACoq_tMeta x + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tSort then + match args with + x :: _ -> ACoq_tSort x + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tProd then + match args with + n :: t :: b :: _ -> ACoq_tProd (n,t,b) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tLambda then + match args with + n :: t :: b :: _ -> ACoq_tLambda (n,t,b) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tLetIn then + match args with + n :: e :: t :: b :: _ -> ACoq_tLetIn (n,e,t,b) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tApp then + match args with + f::xs::_ -> ACoq_tApp (f, from_coq_list xs) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tConst then + match args with + s::u::_ -> ACoq_tConst (s, u) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tInd then + match args with + i::u::_ -> ACoq_tInd (i,u) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tConstructor then + match args with + i::idx::u::_ -> ACoq_tConstruct (i,idx,u) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure: constructor case")) + else if Term.eq_constr h tCase then + match args with + info::ty::d::brs::_ -> ACoq_tCase (from_coq_pair info, ty, d, List.map from_coq_pair (from_coq_list brs)) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tFix then + match args with + bds::i::_ -> + let unquoteFbd b = + let (_,args) = app_full b [] in + match args with + | _(*type*) :: na :: ty :: body :: rarg :: [] -> + { adtype = ty; + adname = na; + adbody = body; + rarg + } + |_ -> raise (Failure " (mkdef must take exactly 5 arguments)") + in + let lbd = List.map unquoteFbd (from_coq_list bds) in + ACoq_tFix (lbd, i) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tCoFix then + match args with + bds::i::_ -> + let unquoteFbd b = + let (_,args) = app_full b [] in + match args with + | _(*type*) :: na :: ty :: body :: rarg :: [] -> + { adtype = ty; + adname = na; + adbody = body; + rarg + } + |_ -> raise (Failure " (mkdef must take exactly 5 arguments)") + in + let lbd = List.map unquoteFbd (from_coq_list bds) in + ACoq_tCoFix (lbd, i) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + else if Term.eq_constr h tProj then + match args with + proj::t::_ -> ACoq_tProj (proj, t) + | _ -> CErrors.user_err (print_term t ++ Pp.str ("has bad structure")) + + else + CErrors.user_err (str"inspect_term: cannot recognize " ++ print_term t) + + let rec unquote_int trm = + let (h,args) = app_full trm [] in + if Term.eq_constr h tO then + 0 + else if Term.eq_constr h tS then + match args with + n :: _ -> 1 + unquote_int n + | _ -> not_supported_verb trm "nat_to_int nil" + else + not_supported_verb trm "nat_to_int" + + let unquote_bool trm = + if Term.eq_constr trm ttrue then + true + else if Term.eq_constr trm tfalse then + false + else not_supported_verb trm "from_bool" + + let unquote_char trm = + let (h,args) = app_full trm [] in + if Term.eq_constr h tAscii then + match args with + a :: b :: c :: d :: e :: f :: g :: h :: _ -> + let bits = List.rev [a;b;c;d;e;f;g;h] in + let v = List.fold_left (fun a n -> (a lsl 1) lor if unquote_bool n then 1 else 0) 0 bits in + char_of_int v + | _ -> assert false + else + not_supported trm + + let unquote_string trm = + let rec go n trm = + let (h,args) = app_full trm [] in + if Term.eq_constr h tEmptyString then + Bytes.create n + else if Term.eq_constr h tString then + match args with + c :: s :: _ -> + let res = go (n + 1) s in + let _ = Bytes.set res n (unquote_char c) in + res + | _ -> bad_term_verb trm "unquote_string" + else + not_supported_verb trm "unquote_string" + in + Bytes.to_string (go 0 trm) + + let unquote_ident trm = + Names.id_of_string (unquote_string trm) + + let unquote_cast_kind trm = + if Term.eq_constr trm kVmCast then + Term.VMcast + else if Term.eq_constr trm kCast then + Term.DEFAULTcast + else if Term.eq_constr trm kRevertCast then + Term.REVERTcast + else if Term.eq_constr trm kNative then + Term.VMcast + else + bad_term trm + + + let unquote_name trm = + let (h,args) = app_full trm [] in + if Term.eq_constr h nAnon then + Names.Anonymous + else if Term.eq_constr h nNamed then + match args with + n :: _ -> Names.Name (unquote_ident n) + | _ -> raise (Failure "ill-typed, expected name") + else + raise (Failure "non-value") + + + (* This code is taken from Pretyping, because it is not exposed globally *) + (* the case for strict universe declarations was removed *) + let get_level evd s = + let names, _ = Global.global_universe_names () in + if CString.string_contains ~where:s ~what:"." then + match List.rev (CString.split '.' s) with + | [] -> CErrors.anomaly (str"Invalid universe name " ++ str s ++ str".") + | n :: dp -> + let num = int_of_string n in + let dp = DirPath.make (List.map Id.of_string dp) in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level + else + try + let level = Evd.universe_of_name evd s in + evd, level + with Not_found -> + try + let id = try Id.of_string s with _ -> raise Not_found in (* Names.Id.of_string can fail if the name is not valid (utf8 ...) *) + evd, snd (Idmap.find id names) + with Not_found -> + Evd.new_univ_level_variable ~name:s Evd.UnivRigid evd + (* end of code from Pretyping *) + + + let rec nat_to_int c = + match Term.kind_of_term c with + | Term.Construct _ -> 0 + | Term.App (s, [| c |]) -> 1 + nat_to_int c + | _ -> bad_term_verb c "unquote_nat" + + let unquote_level evd trm (* of type level *) : Evd.evar_map * Univ.Level.t = + let (h,args) = app_full trm [] in + if Term.eq_constr h lProp then + match args with + | [] -> evd, Univ.Level.prop + | _ -> bad_term_verb trm "unquote_level" + else if Term.eq_constr h lSet then + match args with + | [] -> evd, Univ.Level.set + | _ -> bad_term_verb trm "unquote_level" + else if Term.eq_constr h tLevel then + match args with + | s :: [] -> get_level evd (unquote_string s) + | _ -> bad_term_verb trm "unquote_level" + else if Term.eq_constr h tLevelVar then + match args with + | l :: [] -> evd, Univ.Level.var (nat_to_int l) + | _ -> bad_term_verb trm "unquote_level" + else + not_supported_verb trm "unquote_level" + + let unquote_level_expr evd trm (* of type level *) b (* of type bool *) : Evd.evar_map * Univ.Universe.t= + let evd, l = unquote_level evd trm in + let u = Univ.Universe.make l in + if unquote_bool b then evd, Univ.Universe.super u + else evd, u + + let unquote_universe evd trm (* of type universe *) = + let levels = List.map from_coq_pair (from_coq_list trm) in + let evd, u = match levels with + | [] -> Evd.new_univ_variable (Evd.UnivFlexible false) evd + | (l,b)::q -> List.fold_left (fun (evd,u) (l,b) -> let evd, u' = unquote_level_expr evd l b + in evd, Univ.Universe.sup u u') + (unquote_level_expr evd l b) q + in evd, u + + let unquote_kn (k : quoted_kernel_name) : Libnames.qualid = + let s = unquote_string k in + Libnames.qualid_of_string s + + let unquote_proj (qp : quoted_proj) : (quoted_inductive * quoted_int * quoted_int) = + let (h,args) = app_full qp [] in + match args with + | tyin::tynat::indpars::idx::[] -> + let (h',args') = app_full indpars [] in + (match args' with + | tyind :: tynat :: ind :: n :: [] -> (ind, n, idx) + | _ -> bad_term_verb qp "not a projection") + | _ -> bad_term_verb qp "not a projection" + + let unquote_inductive trm = + let (h,args) = app_full trm [] in + if Term.eq_constr h tmkInd then + match args with + nm :: num :: _ -> + let s = (unquote_string nm) in + let (dp, nm) = split_name s in + (try + match Nametab.locate (Libnames.make_qualid dp nm) with + | Globnames.ConstRef c -> CErrors.user_err (str "this not an inductive constant. use tConst instead of tInd : " ++ str s) + | Globnames.IndRef i -> (fst i, unquote_int num) + | Globnames.VarRef _ -> CErrors.user_err (str "the constant is a variable. use tVar : " ++ str s) + | Globnames.ConstructRef _ -> CErrors.user_err (str "the constant is a consructor. use tConstructor : " ++ str s) + with + Not_found -> CErrors.user_err (str "Constant not found : " ++ str s)) + | _ -> assert false + else + bad_term_verb trm "non-constructor" + + + end @@ -994,108 +1354,203 @@ struct in List.fold_left (fun acc x -> Q.mkExt x acc) (Q.mkIn x) !constants - (* let quote_one_ind envA envC (mi:Entries.one_inductive_entry) = *) - (* let iname = Q.quote_ident mi.mind_entry_typename in *) - (* let arity = quote_term envA mi.mind_entry_arity in *) - (* let templatePoly = Q.quote_bool mi.mind_entry_template in *) - (* let consnames = List.map Q.quote_ident (mi.mind_entry_consnames) in *) - (* let constypes = List.map (quote_term envC) (mi.mind_entry_lc) in *) - (* (iname, arity, templatePoly, consnames, constypes) *) - - (* let process_local_entry *) - (* (f: 'a -> Term.constr option (\* body *\) -> Term.constr (\* type *\) -> Names.Id.t -> Environ.env -> 'a) *) - (* ((env,a):(Environ.env*'a)) *) - (* ((n,le):(Names.Id.t * Entries.local_entry)) *) - (* : (Environ.env * 'a) = *) - (* match le with *) - (* | Entries.LocalAssumEntry t -> (Environ.push_rel (toDecl (Names.Name n,None,t)) env, f a None t n env) *) - (* | Entries.LocalDefEntry b -> *) - (* let typ = getType env b in *) - (* (Environ.push_rel (toDecl (Names.Name n, Some b, typ)) env, f a (Some b) typ n env) *) - - - (* let quote_mind_params env (params:(Names.Id.t * Entries.local_entry) list) = *) - (* let f lr ob t n env = *) - (* match ob with *) - (* | Some b -> (Q.quote_ident n, Left (quote_term env b))::lr *) - (* | None -> *) - (* let sf = getSort env t in *) - (* let t' = castSetProp sf (quote_term env t) in *) - (* (Q.quote_ident n, Right t')::lr in *) - (* let (env, params) = List.fold_left (process_local_entry f) (env,[]) (List.rev params) in *) - (* (env, Q.quote_mind_params (List.rev params)) *) - - (* let mind_params_as_types ((env,t):Environ.env*Term.constr) (params:(Names.Id.t * Entries.local_entry) list) : *) - (* Environ.env*Term.constr = *) - (* List.fold_left (process_local_entry (fun tr ob typ n env -> Term.mkProd_or_LetIn (toDecl (Names.Name n,ob,typ)) tr)) (env,t) *) - (* (List.rev params) *) - - (* let quote_mut_ind env (mi:Declarations.mutual_inductive_body) = *) - (* let t= Discharge.process_inductive ([],Univ.AUContext.empty) (Names.Cmap.empty,Names.Mindmap.empty) mi in *) - (* let mf = Q.quote_mind_finiteness t.mind_entry_finite in *) - (* let mp = (snd (quote_mind_params env (t.mind_entry_params))) in *) - (* (\* before quoting the types of constructors, we need to enrich the environment with the inductives *\) *) - (* let one_arities = *) - (* List.map *) - (* (fun x -> (x.mind_entry_typename, *) - (* snd (mind_params_as_types (env,x.mind_entry_arity) (t.mind_entry_params)))) *) - (* t.mind_entry_inds in *) - (* (\* env for quoting constructors of inductives. First push inductices, then params *\) *) - (* let envC = List.fold_left (fun env p -> Environ.push_rel (toDecl (Names.Name (fst p), None, snd p)) env) env (one_arities) in *) - (* let (envC,_) = List.fold_left (process_local_entry (fun _ _ _ _ _ -> ())) (envC,()) (List.rev (t.mind_entry_params)) in *) - (* (\* env for quoting arities of inductives -- just push the params *\) *) - (* let (envA,_) = List.fold_left (process_local_entry (fun _ _ _ _ _ -> ())) (env,()) (List.rev (t.mind_entry_params)) in *) - (* let is = List.map (quote_one_ind envA envC) t.mind_entry_inds in *) - (* let mpol = Q.quote_bool false in *) - (* Q.quote_mutual_inductive_entry (mf, mp, is, mpol) *) - - (* let quote_entry bypass env evm (name:string) = *) - (* let (dp, nm) = split_name name in *) - (* let entry = *) - (* match Nametab.locate (Libnames.make_qualid dp nm) with *) - (* | Globnames.ConstRef c -> *) - (* let cd = Environ.lookup_constant c env in *) - (* let ty = *) - (* match cd.const_type with *) - (* | RegularArity ty -> quote_term env ty *) - (* | TemplateArity _ -> *) - (* CErrors.user_err (Pp.str "Cannot reify deprecated template-polymorphic constant types") *) - (* in *) - (* let body = match cd.const_body with *) - (* | Undef _ -> None *) - (* | Def cs -> Some (quote_term env (Mod_subst.force_constr cs)) *) - (* | OpaqueDef cs -> *) - (* if bypass *) - (* then Some (quote_term env (Opaqueproof.force_proof (Global.opaque_tables ()) cs)) *) - (* else None *) - (* in Some (Left (ty, body)) *) - - (* | Globnames.IndRef ni -> *) - (* let c = Environ.lookup_mind (fst ni) env in (\* FIX: For efficienctly, we should also export (snd ni)*\) *) - (* let miq = quote_mut_ind env c in *) - (* Some (Right miq) *) - (* | Globnames.ConstructRef _ -> None (\* FIX?: return the enclusing mutual inductive *\) *) - (* | Globnames.VarRef _ -> None *) - (* in Q.quote_entry entry *) -end + let quote_one_ind envA envC (mi:Entries.one_inductive_entry) = + let iname = Q.quote_ident mi.mind_entry_typename in + let arity = quote_term envA mi.mind_entry_arity in + let templatePoly = Q.quote_bool mi.mind_entry_template in + let consnames = List.map Q.quote_ident (mi.mind_entry_consnames) in + let constypes = List.map (quote_term envC) (mi.mind_entry_lc) in + (iname, arity, templatePoly, consnames, constypes) + + let process_local_entry + (f: 'a -> Term.constr option (* body *) -> Term.constr (* type *) -> Names.Id.t -> Environ.env -> 'a) + ((env,a):(Environ.env*'a)) + ((n,le):(Names.Id.t * Entries.local_entry)) + : (Environ.env * 'a) = + match le with + | Entries.LocalAssumEntry t -> (Environ.push_rel (toDecl (Names.Name n,None,t)) env, f a None t n env) + | Entries.LocalDefEntry b -> + let typ = getType env b in + (Environ.push_rel (toDecl (Names.Name n, Some b, typ)) env, f a (Some b) typ n env) + + let quote_mind_params env (params:(Names.Id.t * Entries.local_entry) list) = + let f lr ob t n env = + match ob with + | Some b -> (Q.quote_ident n, Left (quote_term env b))::lr + | None -> + let sf = getSort env t in + let t' = castSetProp sf (quote_term env t) in + (Q.quote_ident n, Right t')::lr in + let (env, params) = List.fold_left (process_local_entry f) (env,[]) (List.rev params) in + (env, Q.quote_mind_params (List.rev params)) + + let mind_params_as_types ((env,t):Environ.env*Term.constr) (params:(Names.Id.t * Entries.local_entry) list) : + Environ.env*Term.constr = + List.fold_left (process_local_entry (fun tr ob typ n env -> Term.mkProd_or_LetIn (toDecl (Names.Name n,ob,typ)) tr)) (env,t) + (List.rev params) + + let quote_mut_ind env (mi:Declarations.mutual_inductive_body) = + let t= Discharge.process_inductive ([],Univ.AUContext.empty) (Names.Cmap.empty,Names.Mindmap.empty) mi in + let mf = Q.quote_mind_finiteness t.mind_entry_finite in + let mp = (snd (quote_mind_params env (t.mind_entry_params))) in + (* before quoting the types of constructors, we need to enrich the environment with the inductives *) + let one_arities = + List.map + (fun x -> (x.mind_entry_typename, + snd (mind_params_as_types (env,x.mind_entry_arity) (t.mind_entry_params)))) + t.mind_entry_inds in + (* env for quoting constructors of inductives. First push inductices, then params *) + let envC = List.fold_left (fun env p -> Environ.push_rel (toDecl (Names.Name (fst p), None, snd p)) env) env (one_arities) in + let (envC,_) = List.fold_left (process_local_entry (fun _ _ _ _ _ -> ())) (envC,()) (List.rev (t.mind_entry_params)) in + (* env for quoting arities of inductives -- just push the params *) + let (envA,_) = List.fold_left (process_local_entry (fun _ _ _ _ _ -> ())) (env,()) (List.rev (t.mind_entry_params)) in + let is = List.map (quote_one_ind envA envC) t.mind_entry_inds in + let uctx = Q.quote_inductive_universes t.mind_entry_universes in + Q.quote_mutual_inductive_entry (mf, mp, is, uctx) + + let quote_entry_aux bypass env evm (name:string) = + let (dp, nm) = split_name name in + let entry = + match Nametab.locate (Libnames.make_qualid dp nm) with + | Globnames.ConstRef c -> + let cd = Environ.lookup_constant c env in + let ty = + match cd.const_type with + | RegularArity ty -> quote_term env ty + | TemplateArity _ -> + CErrors.user_err (Pp.str "Cannot reify deprecated template-polymorphic constant types") + in + let body = match cd.const_body with + | Undef _ -> None + | Def cs -> Some (quote_term env (Mod_subst.force_constr cs)) + | OpaqueDef cs -> + if bypass + then Some (quote_term env (Opaqueproof.force_proof (Global.opaque_tables ()) cs)) + else None + in + let uctx = quote_constant_uctx cd.const_universes in + Some (Left (ty, body, uctx)) + + | Globnames.IndRef ni -> + let c = Environ.lookup_mind (fst ni) env in (* FIX: For efficienctly, we should also export (snd ni)*) + let miq = quote_mut_ind env c in + Some (Right miq) + | Globnames.ConstructRef _ -> None (* FIX?: return the enclusing mutual inductive *) + | Globnames.VarRef _ -> None + in entry + + let quote_entry bypass env evm t = + let entry = quote_entry_aux bypass env evm t in + Q.quote_entry entry + + (* TODO: replace app_full by this abstract version?*) + let rec app_full_abs (trm: Q.t) (acc: Q.t list) = + match Q.inspectTerm trm with + ACoq_tApp (f, xs) -> app_full_abs f (xs @ acc) + | _ -> (trm, acc) + + let str_abs (t: Q.t) : Pp.std_ppcmds = Q.print_term t (* unfold this defn everywhere and delete*) + let not_supported_verb (t: Q.t) s = CErrors.user_err (Pp.(str_abs t ++ Pp.str s)) + let bad_term (t: Q.t) = not_supported_verb t "bad_term" + + (** NOTE: Because the representation is lossy, I should probably + ** come back through elaboration. + ** - This would also allow writing terms with holes + **) -module TermReify = Reify(TemplateCoqQuoter) +let denote_term evdref (trm: Q.t) : Term.constr = + let rec aux (trm: Q.t) : Term.constr = + (*debug (fun () -> Pp.(str "denote_term" ++ spc () ++ Printer.pr_constr trm)) ; *) + match (Q.inspectTerm trm) with + | ACoq_tRel x -> Term.mkRel (Q.unquote_int x + 1) + | ACoq_tVar x -> Term.mkVar (Q.unquote_ident x) + | ACoq_tSort x -> + let evd, u = Q.unquote_universe !evdref x in evdref := evd; Term.mkType u + | ACoq_tCast (t,c,ty) -> Term.mkCast (aux t, Q.unquote_cast_kind c, aux ty) + | ACoq_tProd (n,t,b) -> Term.mkProd (Q.unquote_name n, aux t, aux b) + | ACoq_tLambda (n,t,b) -> Term.mkLambda (Q.unquote_name n, aux t, aux b) + | ACoq_tLetIn (n,e,t,b) -> Term.mkLetIn (Q.unquote_name n, aux e, aux t, aux b) + | ACoq_tApp (f,xs) -> + Term.mkApp (aux f, Array.of_list (List.map aux xs)) + | ACoq_tConst (s,_) -> + (* TODO: unquote universes *) + let s = (Q.unquote_kn s) in + (try + match Nametab.locate s with + | Globnames.ConstRef c -> + EConstr.Unsafe.to_constr (Evarutil.e_new_global evdref (Globnames.ConstRef c)) + | Globnames.IndRef _ -> CErrors.user_err (str "the constant is an inductive. use tInd : " + ++ Pp.str (Libnames.string_of_qualid s)) + | Globnames.VarRef _ -> CErrors.user_err (str "the constant is a variable. use tVar : " ++ Pp.str (Libnames.string_of_qualid s)) + | Globnames.ConstructRef _ -> CErrors.user_err (str "the constant is a consructor. use tConstructor : "++ Pp.str (Libnames.string_of_qualid s)) + with + Not_found -> CErrors.user_err (str "Constant not found : " ++ Pp.str (Libnames.string_of_qualid s))) + | ACoq_tConstruct (i,idx,_) -> + let ind = Q.unquote_inductive i in + Term.mkConstruct (ind, Q.unquote_int idx + 1) + | ACoq_tInd (i, _) -> + let i = Q.unquote_inductive i in + Term.mkInd i + | ACoq_tCase (info, ty, d, brs) -> + let i, _ = info in + let ind = Q.unquote_inductive i in + let ci = Inductiveops.make_case_info (Global.env ()) ind Term.RegularStyle in + let denote_branch br = + let _, br = br in + aux br + in + Term.mkCase (ci, aux ty, aux d, Array.of_list (List.map denote_branch (brs))) + | ACoq_tFix (lbd, i) -> + let (names,types,bodies,rargs) = (List.map (fun p->p.adname) lbd, List.map (fun p->p.adtype) lbd, List.map (fun p->p.adbody) lbd, + List.map (fun p->p.rarg) lbd) in + let (types,bodies) = (List.map aux types, List.map aux bodies) in + let (names,rargs) = (List.map Q.unquote_name names, List.map Q.unquote_int rargs) in + let la = Array.of_list in + Term.mkFix ((la rargs,Q.unquote_int i), (la names, la types, la bodies)) + | ACoq_tCoFix (lbd, i) -> + let (names,types,bodies,rargs) = (List.map (fun p->p.adname) lbd, List.map (fun p->p.adtype) lbd, List.map (fun p->p.adbody) lbd, + List.map (fun p->p.rarg) lbd) in + let (types,bodies) = (List.map aux types, List.map aux bodies) in + let (names,rargs) = (List.map Q.unquote_name names, List.map Q.unquote_int rargs) in + let la = Array.of_list in + Term.mkCoFix (Q.unquote_int i, (la names, la types, la bodies)) + | ACoq_tProj (proj,t) -> + let (ind, _, narg) = Q.unquote_proj proj in (* is narg the correct projection? *) + let ind' = Q.unquote_inductive ind in + let idx = Q.unquote_int narg in + let (mib,_) = Inductive.lookup_mind_specif (Global.env ()) ind' in + let cst = + match mib.mind_record with + | Some (Some (_id, csts, _projs)) -> + assert (Array.length csts > idx); + csts.(idx) + | _ -> not_supported_verb trm "not a primitive record" + in + Term.mkProj (Names.Projection.make cst false, aux t) + | _ -> not_supported_verb trm "big_case" + (* + else if Term.eq_constr h tProj then + match args with + | [ proj ; t ] -> + let (p, narg) = from_coq_pair proj in + let (ind, _) = from_coq_pair p in + let ind' = denote_inductive ind in + let projs = Recordops.lookup_projections ind' in + (match List.nth projs (nat_to_int narg) with + | Some p -> Term.mkProj (Names.Projection.make p false, aux t) + | None -> bad_term trm) + | _ -> raise (Failure "ill-typed (proj)") + else + not_supported_verb trm "big_case" *) + in aux trm + +end +module TermReify = Reify(TemplateCoqQuoter) -let reduce_hnf env evm (trm : Term.constr) = - let trm = Tacred.hnf_constr env evm (EConstr.of_constr trm) in - (evm, EConstr.to_constr evm trm) -let reduce_all env evm ?(red=Genredexpr.Cbv Redops.all_flags) trm = - let red, _ = Redexpr.reduction_of_red_expr env red in - let evm, red = red env evm (EConstr.of_constr trm) in - (evm, EConstr.to_constr evm red) -let rec app_full trm acc = - match Term.kind_of_term trm with - Term.App (f, xs) -> app_full f (Array.to_list xs @ acc) - | _ -> (trm, acc) module Denote = @@ -1103,325 +1558,10 @@ struct open TemplateCoqQuoter - let rec nat_to_int trm = - let (h,args) = app_full trm [] in - if Term.eq_constr h tO then - 0 - else if Term.eq_constr h tS then - match args with - n :: _ -> 1 + nat_to_int n - | _ -> not_supported_verb trm "nat_to_int nil" - else - not_supported_verb trm "nat_to_int" - - let from_bool trm = - if Term.eq_constr trm ttrue then - true - else if Term.eq_constr trm tfalse then - false - else not_supported_verb trm "from_bool" - - let unquote_char trm = - let (h,args) = app_full trm [] in - if Term.eq_constr h tAscii then - match args with - a :: b :: c :: d :: e :: f :: g :: h :: _ -> - let bits = List.rev [a;b;c;d;e;f;g;h] in - let v = List.fold_left (fun a n -> (a lsl 1) lor if from_bool n then 1 else 0) 0 bits in - char_of_int v - | _ -> assert false - else - not_supported trm - - let unquote_string trm = - let rec go n trm = - let (h,args) = app_full trm [] in - if Term.eq_constr h tEmptyString then - Bytes.create n - else if Term.eq_constr h tString then - match args with - c :: s :: _ -> - let res = go (n + 1) s in - let _ = Bytes.set res n (unquote_char c) in - res - | _ -> bad_term_verb trm "unquote_string" - else - not_supported_verb trm "unquote_string" - in - Bytes.to_string (go 0 trm) - - let unquote_ident trm = - Names.id_of_string (unquote_string trm) - - let unquote_cast_kind trm = - if Term.eq_constr trm kVmCast then - Term.VMcast - else if Term.eq_constr trm kCast then - Term.DEFAULTcast - else if Term.eq_constr trm kRevertCast then - Term.REVERTcast - else if Term.eq_constr trm kNative then - Term.VMcast - else - bad_term trm - - - let unquote_name trm = - let (h,args) = app_full trm [] in - if Term.eq_constr h nAnon then - Names.Anonymous - else if Term.eq_constr h nNamed then - match args with - n :: _ -> Names.Name (unquote_ident n) - | _ -> raise (Failure "ill-typed, expected name") - else - raise (Failure "non-value") - - - - let from_coq_pair trm = - let (h,args) = app_full trm [] in - if Term.eq_constr h c_pair then - match args with - _ :: _ :: x :: y :: [] -> (x, y) - | _ -> bad_term trm - else - not_supported_verb trm "from_coq_pair" - - - let rec from_coq_list trm = - let (h,args) = app_full trm [] in - if Term.eq_constr h c_nil then [] - else if Term.eq_constr h c_cons then - match args with - _ :: x :: xs :: _ -> x :: from_coq_list xs - | _ -> bad_term trm - else - not_supported_verb trm "from_coq_list" - - - (* This code is taken from Pretyping, because it is not exposed globally *) - (* the case for strict universe declarations was removed *) - let get_level evd s = - let names, _ = Global.global_universe_names () in - if CString.string_contains ~where:s ~what:"." then - match List.rev (CString.split '.' s) with - | [] -> CErrors.anomaly (str"Invalid universe name " ++ str s ++ str".") - | n :: dp -> - let num = int_of_string n in - let dp = DirPath.make (List.map Id.of_string dp) in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - else - try - let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in (* Names.Id.of_string can fail if the name is not valid (utf8 ...) *) - evd, snd (Idmap.find id names) - with Not_found -> - Evd.new_univ_level_variable ~name:s Evd.UnivRigid evd - (* end of code from Pretyping *) - - - - let unquote_level evd trm (* of type level *) : Evd.evar_map * Univ.Level.t = - let (h,args) = app_full trm [] in - if Term.eq_constr h lProp then - match args with - | [] -> evd, Univ.Level.prop - | _ -> bad_term_verb trm "unquote_level" - else if Term.eq_constr h lSet then - match args with - | [] -> evd, Univ.Level.set - | _ -> bad_term_verb trm "unquote_level" - else if Term.eq_constr h tLevel then - match args with - | s :: [] -> get_level evd (unquote_string s) - | _ -> bad_term_verb trm "unquote_level" - else if Term.eq_constr h tLevelVar then - match args with - | l :: [] -> evd, Univ.Level.var (nat_to_int l) - | _ -> bad_term_verb trm "unquote_level" - else - not_supported_verb trm "unquote_level" - - let unquote_level_expr evd trm (* of type level *) b (* of type bool *) : Evd.evar_map * Univ.Universe.t= - let evd, l = unquote_level evd trm in - let u = Univ.Universe.make l in - if from_bool b then evd, Univ.Universe.super u - else evd, u - - let unquote_universe evd trm (* of type universe *) = - let levels = List.map from_coq_pair (from_coq_list trm) in - let evd, u = match levels with - | [] -> Evd.new_univ_variable (Evd.UnivFlexible false) evd - | (l,b)::q -> List.fold_left (fun (evd,u) (l,b) -> let evd, u' = unquote_level_expr evd l b - in evd, Univ.Universe.sup u u') - (unquote_level_expr evd l b) q - in evd, u - - - - let denote_inductive trm = - let (h,args) = app_full trm [] in - if Term.eq_constr h tmkInd then - match args with - nm :: num :: _ -> - let s = (unquote_string nm) in - let (dp, nm) = split_name s in - (try - match Nametab.locate (Libnames.make_qualid dp nm) with - | Globnames.ConstRef c -> CErrors.user_err (str "this not an inductive constant. use tConst instead of tInd : " ++ str s) - | Globnames.IndRef i -> (fst i, nat_to_int num) - | Globnames.VarRef _ -> CErrors.user_err (str "the constant is a variable. use tVar : " ++ str s) - | Globnames.ConstructRef _ -> CErrors.user_err (str "the constant is a consructor. use tConstructor : " ++ str s) - with - Not_found -> CErrors.user_err (str "Constant not found : " ++ str s)) - | _ -> assert false - else - bad_term_verb trm "non-constructor" - - (** NOTE: Because the representation is lossy, I should probably ** come back through elaboration. ** - This would also allow writing terms with holes **) - let denote_term evdref trm = - let rec aux trm = - debug (fun () -> Pp.(str "denote_term" ++ spc () ++ Printer.pr_constr trm)) ; - let (h,args) = app_full trm [] in - if Term.eq_constr h tRel then - match args with - x :: _ -> - Term.mkRel (nat_to_int x + 1) - | _ -> raise (Failure "ill-typed") - else if Term.eq_constr h tVar then - match args with - x :: _ -> Term.mkVar (unquote_ident x) - | _ -> raise (Failure "ill-typed") - else if Term.eq_constr h tSort then - match args with - x :: _ -> let evd, u = unquote_universe !evdref x in evdref := evd; Term.mkType u - | _ -> raise (Failure "ill-typed") - else if Term.eq_constr h tCast then - match args with - t :: c :: ty :: _ -> - Term.mkCast (aux t, unquote_cast_kind c, aux ty) - | _ -> raise (Failure "ill-typed") - else if Term.eq_constr h tProd then - match args with - n :: t :: b :: _ -> - Term.mkProd (unquote_name n, aux t, aux b) - | _ -> raise (Failure "ill-typed (product)") - else if Term.eq_constr h tLambda then - match args with - n :: t :: b :: _ -> - Term.mkLambda (unquote_name n, aux t, aux b) - | _ -> raise (Failure "ill-typed (lambda)") - else if Term.eq_constr h tLetIn then - match args with - n :: e :: t :: b :: _ -> - Term.mkLetIn (unquote_name n, aux e, aux t, aux b) - | _ -> raise (Failure "ill-typed (let-in)") - else if Term.eq_constr h tApp then - match args with - f :: xs :: _ -> - Term.mkApp (aux f, - Array.of_list (List.map aux (from_coq_list xs))) - | _ -> raise (Failure "ill-typed (app)") - else if Term.eq_constr h tConst then - match args with - s :: u :: [] -> - (* TODO: unquote universes *) - let s = (unquote_string s) in - let (dp, nm) = split_name s in - (try - match Nametab.locate (Libnames.make_qualid dp nm) with - | Globnames.ConstRef c -> - EConstr.Unsafe.to_constr (Evarutil.e_new_global evdref (Globnames.ConstRef c)) - | Globnames.IndRef _ -> CErrors.user_err (str "the constant is an inductive. use tInd : " ++ str s) - | Globnames.VarRef _ -> CErrors.user_err (str "the constant is a variable. use tVar : " ++ str s) - | Globnames.ConstructRef _ -> CErrors.user_err (str "the constant is a consructor. use tConstructor : " ++ str s) - with - Not_found -> CErrors.user_err (str "Constant not found : " ++ str s)) - | _ -> raise (Failure "ill-typed (tConst)") - else if Term.eq_constr h tConstructor then - match args with - i :: idx :: _ -> - let i = denote_inductive i in - Term.mkConstruct (i, nat_to_int idx + 1) - | _ -> raise (Failure "ill-typed (constructor)") - else if Term.eq_constr h tInd then - match args with - i :: _ -> - let i = denote_inductive i in - Term.mkInd i - | _ -> raise (Failure "ill-typed (inductive)") - else if Term.eq_constr h tCase then - match args with - info :: ty :: d :: brs :: _ -> - let i, _ = from_coq_pair info in - let ind = denote_inductive i in - let ci = Inductiveops.make_case_info (Global.env ()) ind Term.RegularStyle in - let denote_branch br = - let _, br = from_coq_pair br in - aux br - in - Term.mkCase (ci, aux ty, aux d, - Array.of_list (List.map denote_branch (from_coq_list brs))) - | _ -> raise (Failure "ill-typed (case)") - else if Term.eq_constr h tFix then - match args with - | bds :: i :: _ -> - let unquoteFbd b : ((Term.constr * Term.constr) * (Term.constr * Term.constr)) = - let (_,args) = app_full b [] in - match args with - | _(*type*)::a::b::c::d::[] -> ((a,b),(c,d)) - |_ -> raise (Failure " (mkdef must take exactly 5 arguments)") - in - let lbd = List.map unquoteFbd (from_coq_list bds) in - let (p1,p2) = (List.map fst lbd, List.map snd lbd) in - let (names,types,bodies,rargs) = (List.map fst p1, List.map snd p1, List.map fst p2, List.map snd p2) in - let (types,bodies) = (List.map aux types, List.map aux bodies) in - let (names,rargs) = (List.map unquote_name names, List.map nat_to_int rargs) in - let la = Array.of_list in - Term.mkFix ((la rargs,nat_to_int i), (la names, la types, la bodies)) - | _ -> raise (Failure "tFix takes exactly 2 arguments") - else if Term.eq_constr h tCoFix then - match args with - | bds :: i :: _ -> - let unquoteFbd b : (Term.constr * Term.constr * Term.constr) = - let (_,args) = app_full b [] in - match args with - | _(*type*)::a::b::c::d::[] -> ((a,b,c)) - |_ -> raise (Failure " (mkdef must take exactly 5 arguments)") - in - let lbd = List.map unquoteFbd (from_coq_list bds) in - let (names,types,bodies) = CList.split3 lbd in - let (types,bodies) = (List.map aux types, List.map aux bodies) in - let names = List.map unquote_name names in - let la = Array.of_list in - Term.mkCoFix (nat_to_int i, (la names, la types, la bodies)) - | _ -> raise (Failure "tFix takes exactly 2 arguments") - else if Term.eq_constr h tProj then - match args with - | [ proj ; t ] -> - let (p, narg) = from_coq_pair proj in - let (ind, _) = from_coq_pair p in - let ind' = denote_inductive ind in - let projs = Recordops.lookup_projections ind' in - (match List.nth projs (nat_to_int narg) with - | Some p -> Term.mkProj (Names.Projection.make p false, aux t) - | None -> bad_term trm) - | _ -> raise (Failure "ill-typed (proj)") - else - not_supported_verb trm "big_case" - in aux trm @@ -1441,8 +1581,8 @@ struct let (h,args) = app_full trm [] in match args with x :: [] -> - if Term.eq_constr h tLocalDef then Entries.LocalDefEntry (denote_term evdref x) - else (if Term.eq_constr h tLocalAssum then Entries.LocalAssumEntry (denote_term evdref x) else bad_term trm) + if Term.eq_constr h tLocalDef then Entries.LocalDefEntry (TermReify.denote_term evdref x) + else (if Term.eq_constr h tLocalAssum then Entries.LocalAssumEntry (TermReify.denote_term evdref x) else bad_term trm) | _ -> bad_term trm let denote_mind_entry_finite trm = @@ -1468,45 +1608,75 @@ struct else not_supported_verb trm "unqote_map_option" + let denote_ucontext (trm : Term.constr) : Univ.universe_context = + Univ.UContext.empty (* FIXME *) - let denote_universe_context (trm : Term.constr) : Univ.universe_context = - Univ.UContext.empty (* FIXME !!! *) - + let denote_universe_context (trm : Term.constr) : bool * Univ.universe_context = + let (h, args) = app_full trm [] in + let b = + if Term.eq_constr h cMonomorphic_ctx then Some false + else if Term.eq_constr h cPolymorphic_ctx then Some true + else None + in + match b, args with + | Some poly, ctx :: [] -> + poly, denote_ucontext ctx + | _, _ -> bad_term trm + + let denote_mind_entry_universes trm = + match denote_universe_context trm with + | false, ctx -> Monomorphic_ind_entry ctx + | true, ctx -> Polymorphic_ind_entry ctx + + (* let denote_inductive_first trm = + * let (h,args) = app_full trm [] in + * if Term.eq_constr h tmkInd then + * match args with + * nm :: num :: _ -> + * let s = (unquote_string nm) in + * let (dp, nm) = split_name s in + * (try + * match Nametab.locate (Libnames.make_qualid dp nm) with + * | Globnames.ConstRef c -> CErrors.user_err (str "this not an inductive constant. use tConst instead of tInd : " ++ str s) + * | Globnames.IndRef i -> (fst i, nat_to_int num) + * | Globnames.VarRef _ -> CErrors.user_err (str "the constant is a variable. use tVar : " ++ str s) + * | Globnames.ConstructRef _ -> CErrors.user_err (str "the constant is a consructor. use tConstructor : " ++ str s) + * with + * Not_found -> CErrors.user_err (str "Constant not found : " ++ str s)) + * | _ -> assert false + * else + * bad_term_verb trm "non-constructor" *) let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (body: Term.constr) : unit = - let (evm,body) = reduce_all env evm body in - let (_,args) = app_full body [] in (* check that the first component is Build_mut_ind .. *) - let evdref = ref evm in - let one_ind b1 : Entries.one_inductive_entry = - let (_,args) = app_full b1 [] in (* check that the first component is Build_one_ind .. *) - match args with - | mt::ma::mtemp::mcn::mct::[] -> - { - mind_entry_typename = unquote_ident mt; - mind_entry_arity = denote_term evdref ma; - mind_entry_template = from_bool mtemp; - mind_entry_consnames = List.map unquote_ident (from_coq_list mcn); - mind_entry_lc = List.map (denote_term evdref) (from_coq_list mct) - } - | _ -> raise (Failure "ill-typed one_inductive_entry") - in - let mut_ind mr mf mp mi mpol uctx mpr : Entries.mutual_inductive_entry = - { - mind_entry_record = unquote_map_option (unquote_map_option unquote_ident) mr; - mind_entry_finite = denote_mind_entry_finite mf; (* inductive *) - mind_entry_params = List.map (fun p -> let (l,r) = (from_coq_pair p) in (unquote_ident l, (denote_local_entry evdref r))) - (List.rev (from_coq_list mp)); - mind_entry_inds = List.map one_ind (from_coq_list mi); - (* mind_entry_polymorphic = from_bool mpol; *) - mind_entry_universes = - (let uctx = denote_universe_context uctx in - if from_bool mpol then Polymorphic_ind_entry uctx - else Monomorphic_ind_entry uctx); - mind_entry_private = unquote_map_option from_bool mpr (*mpr*) - } in + let (evm,body) = reduce_all env evm body in + let (_,args) = app_full body [] in (* check that the first component is Build_mut_ind .. *) + let evdref = ref evm in + let one_ind b1 : Entries.one_inductive_entry = + let (_,args) = app_full b1 [] in (* check that the first component is Build_one_ind .. *) + match args with + | mt::ma::mtemp::mcn::mct::[] -> + { + mind_entry_typename = unquote_ident mt; + mind_entry_arity = TermReify.denote_term evdref ma; + mind_entry_template = TemplateCoqQuoter.unquote_bool mtemp; + mind_entry_consnames = List.map unquote_ident (from_coq_list mcn); + mind_entry_lc = List.map (TermReify.denote_term evdref) (from_coq_list mct) + } + | _ -> raise (Failure "ill-typed one_inductive_entry") + in + let mut_ind mr mf mp mi uctx mpr : Entries.mutual_inductive_entry = + { + mind_entry_record = unquote_map_option (unquote_map_option unquote_ident) mr; + mind_entry_finite = denote_mind_entry_finite mf; (* inductive *) + mind_entry_params = List.map (fun p -> let (l,r) = (from_coq_pair p) in (unquote_ident l, (denote_local_entry evdref r))) + (List.rev (from_coq_list mp)); + mind_entry_inds = List.map one_ind (from_coq_list mi); + mind_entry_universes = denote_mind_entry_universes uctx; + mind_entry_private = unquote_map_option TemplateCoqQuoter.unquote_bool mpr (*mpr*) + } in match args with - mr::mf::mp::mi::mpol::univs::mpr::[] -> - ignore(Command.declare_mutual_inductive_with_eliminations (mut_ind mr mf mp mi mpol univs mpr) [] []) + mr::mf::mp::mi::univs::mpr::[] -> + ignore(Command.declare_mutual_inductive_with_eliminations (mut_ind mr mf mp mi univs mpr) [] []) | _ -> raise (Failure "ill-typed mutual_inductive_entry") @@ -1514,6 +1684,13 @@ struct CErrors.user_err (str (s ^ " must take " ^ (string_of_int k) ^ " argument" ^ (if k > 0 then "s" else "") ^ ".") ++ str "Please file a bug with Template-Coq.") + + let monad_failure_full s k prg = + CErrors.user_err + (str (s ^ " must take " ^ (string_of_int k) ^ " argument" ^ (if k > 0 then "s" else "") ^ ".") ++ + str "While trying to run: " ++ fnl () ++ print_term prg ++ fnl () ++ + str "Please file a bug with Template-Coq.") + let rec run_template_program_rec (k : Evd.evar_map * Term.constr -> unit) ((evm, pgm) : Evd.evar_map * Term.constr) : unit = let env = Global.env () in let (evm, pgm) = reduce_hnf env evm pgm in @@ -1526,7 +1703,7 @@ struct match args with | _::_::a::f::[] -> run_template_program_rec (fun (evm, ar) -> run_template_program_rec k (evm, Term.mkApp (f, [|ar|]))) (evm, a) - | _ -> monad_failure "tmBind" 4 + | _ -> monad_failure_full "tmBind" 4 pgm else if Term.eq_constr coConstr tmDefinition then match args with | name::typ::body::[] -> @@ -1572,7 +1749,7 @@ struct let (evm, name) = reduce_all env evm name in let (evm, def) = reduce_all env evm body in let evdref = ref evm in - let trm = denote_term evdref def in + let trm = TermReify.denote_term evdref def in let ty = Typing.e_type_of env evdref (EConstr.of_constr trm) in let evm = !evdref in let _ = Declare.declare_definition ~kind:Decl_kinds.Definition (unquote_ident name) (trm, Evd.universe_context_set evm) in @@ -1615,28 +1792,14 @@ struct let (evm, name) = reduce_all env evm name in let name = unquote_string name in let (evm, b) = reduce_all env evm b in - let bypass = from_bool b in - let (dp, nm) = split_name name in - let entry = (* todo: this should be defined in the quoter module *) - match Nametab.locate (Libnames.make_qualid dp nm) with - | Globnames.ConstRef c -> - let cd = Environ.lookup_constant c env in - let (polym, univs) = match cd.const_universes with - | Monomorphic_const ctx -> (false, quote_univ_context ctx) - | Polymorphic_const ctx -> (true, quote_abstract_univ_context ctx) in - let ty = match cd.const_type with - | RegularArity ty -> TermReify.quote_term env ty - | TemplateArity _ -> CErrors.user_err (Pp.str "Cannot reify deprecated template-polymorphic constant types") - in - let body = match cd.const_body with - | Def cs -> Some (TermReify.quote_term env (Mod_subst.force_constr cs)) - | OpaqueDef cs when bypass -> Some (TermReify.quote_term env (Opaqueproof.force_proof (Global.opaque_tables ()) cs)) - | _ -> None - in - (match body with - | Some body -> Term.mkApp (cDefinitionEntry, [| Term.mkApp (cDefinition_entry, [|ty;body; quote_bool polym; univs; tfalse|]) |]) - | None -> Term.mkApp (cParameterEntry, [| Term.mkApp (cParameter_entry, [|ty; quote_bool polym; univs; tfalse|]) |])) - | _ -> CErrors.user_err (str name ++ str " does not seem to be a constant.") in + let bypass = TemplateCoqQuoter.unquote_bool b in + let entry = TermReify.quote_entry_aux bypass env evm name in + let entry = + match entry with + | Some (Left cstentry) -> TemplateCoqQuoter.quote_constant_entry cstentry + | Some (Right _) -> CErrors.user_err (str name ++ str " refers to an inductive") + | None -> bad_term_verb coConstr "anomaly in QuoteConstant" + in k (evm, entry) | _ -> monad_failure "tmQuoteConstant" 2 else if Term.eq_constr coConstr tmQuoteUniverses then @@ -1687,7 +1850,7 @@ struct | t::[] -> let (evm, t) = reduce_all env evm t in let evdref = ref evm in - let t' = denote_term evdref t in + let t' = TermReify.denote_term evdref t in let evm = !evdref in let typ = EConstr.to_constr evm (Retyping.get_type_of env evm (EConstr.of_constr t')) in (* todo: we could declare a new universe <= Coq.Init.Specif.7 or 8 instead of using [texistT_typed_term] *) @@ -1702,7 +1865,7 @@ struct | typ::t::[] -> let (evm, t) = reduce_all env evm t in let evdref = ref evm in - let t' = denote_term evdref t in + let t' = TermReify.denote_term evdref t in let t' = Typing.e_solve_evars env evdref (EConstr.of_constr t') in Typing.e_check env evdref t' (EConstr.of_constr typ) ; let t' = EConstr.to_constr !evdref t' in @@ -1773,7 +1936,7 @@ TACTIC EXTEND denote_term let env = Proofview.Goal.env gl in let evm = Proofview.Goal.sigma gl in let evdref = ref evm in - let c = Denote.denote_term evdref (EConstr.to_constr evm c) in + let c = TermReify.denote_term evdref (EConstr.to_constr evm c) in (* TODO : not the right way of retype things *) let def' = Constrextern.extern_constr true env !evdref (EConstr.of_constr c) in let def = Constrintern.interp_constr env !evdref def' in @@ -1823,7 +1986,7 @@ VERNAC COMMAND EXTEND Unquote_vernac CLASSIFIED AS SIDEFF let (evm, env) = Lemmas.get_current_context () in let (trm, uctx) = Constrintern.interp_constr env evm def in let evdref = ref (Evd.from_ctx uctx) in - let trm = Denote.denote_term evdref trm in + let trm = TermReify.denote_term evdref trm in let _ = Declare.declare_definition ~kind:Decl_kinds.Definition name (trm, Evd.universe_context_set !evdref) in () ] END;; @@ -1837,7 +2000,7 @@ VERNAC COMMAND EXTEND Unquote_vernac_red CLASSIFIED AS SIDEFF let (evm,rd) = Tacinterp.interp_redexp env evm rd in let (evm,trm) = reduce_all env evm ~red:rd trm in let evdref = ref evm in - let trm = Denote.denote_term evdref trm in + let trm = TermReify.denote_term evdref trm in let _ = Declare.declare_definition ~kind:Decl_kinds.Definition name (trm, Evd.universe_context_set !evdref) in () ] END;; diff --git a/src/reify.mli b/src/reify.mli index 826fe85e2..d6d8b21ba 100644 --- a/src/reify.mli +++ b/src/reify.mli @@ -1,6 +1,29 @@ type ('a,'b) sum = Left of 'a | Right of 'b +type ('term, 'name, 'nat) adef = { adname : 'name; adtype : 'term; adbody : 'term; rarg : 'nat } + +type ('term, 'name, 'nat) amfixpoint = ('term, 'name, 'nat) adef list + +type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive, 'universe_instance, 'projection) structure_of_term = + | ACoq_tRel of 'nat + | ACoq_tVar of 'ident + | ACoq_tMeta of 'nat + | ACoq_tEvar of 'nat * 'term list + | ACoq_tSort of 'quoted_sort + | ACoq_tCast of 'term * 'cast_kind * 'term + | ACoq_tProd of 'name * 'term * 'term + | ACoq_tLambda of 'name * 'term * 'term + | ACoq_tLetIn of 'name * 'term * 'term * 'term + | ACoq_tApp of 'term * 'term list + | ACoq_tConst of 'kername * 'universe_instance + | ACoq_tInd of 'inductive * 'universe_instance + | ACoq_tConstruct of 'inductive * 'nat * 'universe_instance + | ACoq_tCase of ('inductive * 'nat) * 'term * 'term * ('nat * 'term) list + | ACoq_tProj of 'projection * 'term + | ACoq_tFix of ('term, 'name, 'nat) amfixpoint * 'nat + | ACoq_tCoFix of ('term, 'name, 'nat) amfixpoint * 'nat + module type Quoter = sig type t @@ -19,10 +42,11 @@ module type Quoter = sig type quoted_univ_instance type quoted_univ_constraints type quoted_univ_context + type quoted_inductive_universes type quoted_mind_params type quoted_ind_entry = quoted_ident * t * quoted_bool * quoted_ident list * t list - type quoted_definition_entry = t * t option + type quoted_definition_entry = t * t option * quoted_univ_context type quoted_mind_entry type quoted_mind_finiteness type quoted_entry @@ -46,14 +70,15 @@ module type Quoter = sig val quote_univ_constraints : Univ.Constraint.t -> quoted_univ_constraints val quote_univ_context : Univ.UContext.t -> quoted_univ_context val quote_abstract_univ_context : Univ.AUContext.t -> quoted_univ_context + val quote_inductive_universes : Entries.inductive_universes -> quoted_inductive_universes + val quote_mind_params : (quoted_ident * (t,t) sum) list -> quoted_mind_params + val quote_mind_finiteness : Decl_kinds.recursivity_kind -> quoted_mind_finiteness + val quote_mutual_inductive_entry : + quoted_mind_finiteness * quoted_mind_params * quoted_ind_entry list * + quoted_inductive_universes -> + quoted_mind_entry - (* val quote_mind_params : (quoted_ident * (t,t) sum) list -> quoted_mind_params *) - (* val quote_mind_finiteness : Decl_kinds.recursivity_kind -> quoted_mind_finiteness *) - (* val quote_mutual_inductive_entry : *) - (* quoted_mind_finiteness * quoted_mind_params * quoted_ind_entry list * quoted_bool -> *) - (* quoted_mind_entry *) - - (* val quote_entry : (quoted_definition_entry, quoted_mind_entry) sum option -> quoted_entry *) + val quote_entry : (quoted_definition_entry, quoted_mind_entry) sum option -> quoted_entry val quote_proj : quoted_inductive -> quoted_int -> quoted_int -> quoted_proj val mkName : quoted_ident -> quoted_name @@ -91,6 +116,22 @@ module type Quoter = sig val mkExt : quoted_decl -> quoted_program -> quoted_program val mkIn : t -> quoted_program + val unquote_ident : quoted_ident -> Id.t + val unquote_name : quoted_name -> Name.t + val unquote_int : quoted_int -> int + val unquote_bool : quoted_bool -> bool + (* val unquote_sort : quoted_sort -> Sorts.t *) + (* val unquote_sort_family : quoted_sort_family -> Sorts.family *) + val unquote_cast_kind : quoted_cast_kind -> Constr.cast_kind + val unquote_kn : quoted_kernel_name -> Libnames.qualid + val unquote_inductive : quoted_inductive -> Names.inductive + (*val unquote_univ_instance : quoted_univ_instance -> Univ.Instance.t *) + val unquote_proj : quoted_proj -> (quoted_inductive * quoted_int * quoted_int) + val unquote_universe : Evd.evar_map -> quoted_sort -> Evd.evar_map * Univ.Universe.t + val print_term : t -> Pp.std_ppcmds + + (* val representsIndConstuctor : quoted_inductive -> Term.constr -> bool *) + val inspectTerm : t -> (t, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_univ_instance, quoted_proj) structure_of_term end module Reify(Q : Quoter) : sig diff --git a/src/template_coq.ml4 b/src/template_coq.ml4 index 0600cc3c2..6f002819f 100644 --- a/src/template_coq.ml4 +++ b/src/template_coq.ml4 @@ -13,6 +13,16 @@ let quote_string s = else aux (s.[i] :: acc) (i - 1) in aux [] (String.length s - 1) +let unquote_string l = + let buf = Bytes.create (List.length l) in + let rec aux i = function + | [] -> () + | c :: cs -> + Bytes.set buf i c; aux (succ i) cs + in + aux 0 l; + Bytes.to_string buf + module TemplateASTQuoter = struct type t = term @@ -31,10 +41,11 @@ struct type quoted_univ_instance = Univ0.Instance.t type quoted_univ_constraints = Univ0.constraints type quoted_univ_context = Univ0.universe_context + type quoted_inductive_universes = quoted_univ_context type quoted_mind_params = (ident * local_entry) list type quoted_ind_entry = quoted_ident * t * quoted_bool * quoted_ident list * t list - type quoted_definition_entry = t * t option + type quoted_definition_entry = t * t option * quoted_univ_context type quoted_mind_entry = mutual_inductive_entry type quoted_mind_finiteness = recursivity_kind type quoted_entry = (constant_entry, quoted_mind_entry) sum option @@ -74,10 +85,6 @@ struct (l', b')) levels - let quote_univ_instance u = - let arr = Univ.Instance.to_array u in - CArray.map_to_list quote_level arr - let quote_sort s = quote_universe (Sorts.univ_of_sort s) @@ -124,7 +131,8 @@ struct ((quote_level l, quote_constraint_type ct), quote_level l') let quote_univ_instance (i : Univ.Instance.t) : quoted_univ_instance = - CArray.map_to_list quote_level (Univ.Instance.to_array i) + let arr = Univ.Instance.to_array i in + CArray.map_to_list quote_level arr let quote_univ_constraints (c : Univ.Constraint.t) : quoted_univ_constraints = List.map quote_univ_constraint (Univ.Constraint.elements c) @@ -134,12 +142,21 @@ struct let constraints = Univ.UContext.constraints uctx in Univ0.Monomorphic_ctx (quote_univ_instance levels, quote_univ_constraints constraints) - let quote_abstract_univ_context (uctx : Univ.AUContext.t) : quoted_univ_context = - let uctx = Univ.AUContext.repr uctx in + let quote_abstract_univ_context_aux uctx : quoted_univ_context = let levels = Univ.UContext.instance uctx in let constraints = Univ.UContext.constraints uctx in Univ0.Polymorphic_ctx (quote_univ_instance levels, quote_univ_constraints constraints) + let quote_abstract_univ_context (uctx : Univ.AUContext.t) = + let uctx = Univ.AUContext.repr uctx in + quote_abstract_univ_context_aux uctx + + let quote_inductive_universes = function + | Entries.Monomorphic_ind_entry ctx -> quote_univ_context ctx + | Entries.Polymorphic_ind_entry ctx -> quote_abstract_univ_context_aux ctx + | Entries.Cumulative_ind_entry ctx -> + quote_abstract_univ_context_aux (Univ.CumulativityInfo.univ_context ctx) + let rec seq f t = if f < t then f :: seq (f + 1) t @@ -196,47 +213,133 @@ struct let mkIn c = PIn c - (* let quote_mind_finiteness = function *) - (* | Decl_kinds.Finite -> Finite *) - (* | Decl_kinds.CoFinite -> CoFinite *) - (* | Decl_kinds.BiFinite -> BiFinite *) - - (* let quote_mind_params l = *) - (* let map (id, body) = *) - (* match body with *) - (* | Left ty -> (id, LocalAssum ty) *) - (* | Right trm -> (id, LocalDef trm) *) - (* in List.map map l *) - - (* let quote_one_inductive_entry (id, ar, b, consnames, constypes) = *) - (* { mind_entry_typename = id; *) - (* mind_entry_arity = ar; *) - (* mind_entry_template = b; *) - (* mind_entry_consnames = consnames; *) - (* mind_entry_lc = constypes } *) - - (* let quote_mutual_inductive_entry (mf, mp, is, poly, univs) = *) - (* { mind_entry_record = None; *) - (* mind_entry_finite = mf; *) - (* mind_entry_params = mp; *) - (* mind_entry_inds = List.map quote_one_inductive_entry is; *) - (* mind_entry_polymorphic = poly; *) - (* mind_entry_universes = univs; *) - (* mind_entry_private = None } *) - - (* let quote_entry e = *) - (* match e with *) - (* | Some (Left (ty, body)) -> *) - (* let entry = match body with *) - (* | None -> ParameterEntry ty *) - (* | Some b -> DefinitionEntry { definition_entry_type = ty; *) - (* definition_entry_body = b } *) - (* in Some (Left entry) *) - (* | Some (Right mind_entry) -> *) - (* Some (Right mind_entry) *) - (* | None -> None *) + let quote_mind_finiteness = function + | Decl_kinds.Finite -> Finite + | Decl_kinds.CoFinite -> CoFinite + | Decl_kinds.BiFinite -> BiFinite + + let quote_mind_params l = + let map (id, body) = + match body with + | Left ty -> (id, LocalAssum ty) + | Right trm -> (id, LocalDef trm) + in List.map map l + + let quote_one_inductive_entry (id, ar, b, consnames, constypes) = + { mind_entry_typename = id; + mind_entry_arity = ar; + mind_entry_template = b; + mind_entry_consnames = consnames; + mind_entry_lc = constypes } + + let quote_mutual_inductive_entry (mf, mp, is, univs) = + { mind_entry_record = None; + mind_entry_finite = mf; + mind_entry_params = mp; + mind_entry_inds = List.map quote_one_inductive_entry is; + mind_entry_universes = univs; + mind_entry_private = None } + + let quote_entry e = + match e with + | Some (Left (ty, body, ctx)) -> + let entry = match body with + | None -> ParameterEntry { parameter_entry_type = ty; + parameter_entry_universes = ctx } + | Some b -> DefinitionEntry { definition_entry_type = ty; + definition_entry_body = b; + definition_entry_universes = ctx; + definition_entry_opaque = false } + in Some (Left entry) + | Some (Right mind_entry) -> + Some (Right mind_entry) + | None -> None + + let inspectTerm (t : term) : (term, quoted_int, quoted_ident, quoted_name, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_univ_instance, quoted_proj) structure_of_term = + match t with + | Coq_tRel n -> ACoq_tRel n + (* so on *) + | _ -> failwith "not yet implemented" + + + + + let unquote_ident (qi: quoted_ident) : Id.t = + let s = unquote_string qi in + Id.of_string s + + let unquote_name (q: quoted_name) : Name.t = + match q with + | Coq_nAnon -> Anonymous + | Coq_nNamed n -> Name (unquote_ident n) + + let rec unquote_int (q: quoted_int) : int = + match q with + | Datatypes.O -> 0 + | Datatypes.S x -> succ (unquote_int x) + + let unquote_bool (q : quoted_bool) : bool = q + + (* val unquote_sort : quoted_sort -> Sorts.t *) + (* val unquote_sort_family : quoted_sort_family -> Sorts.family *) + let unquote_cast_kind (q : quoted_cast_kind) : Constr.cast_kind = + match q with + | VmCast -> VMcast + | NativeCast -> NATIVEcast + | Cast -> DEFAULTcast + | RevertCast -> REVERTcast + + let unquote_kn (q: quoted_kernel_name) : Libnames.qualid = + let s = unquote_string q in + Libnames.qualid_of_string s + + let unquote_inductive (q: quoted_inductive) : Names.inductive = + let { inductive_mind = na; inductive_ind = i } = q in + let comps = CString.split '.' (unquote_string na) in + let comps = List.map Id.of_string comps in + let id, dp = CList.sep_last comps in + let dp = DirPath.make dp in + let mind = Globnames.encode_mind dp id in + (mind, unquote_int i) + + (*val unquote_univ_instance : quoted_univ_instance -> Univ.Instance.t *) + let unquote_proj (q : quoted_proj) : (quoted_inductive * quoted_int * quoted_int) = + let (ind, ps), idx = q in + (ind, ps, idx) + + let unquote_level (trm : Univ0.Level.t) : Univ.Level.t = + match trm with + | Univ0.Level.Coq_lProp -> Univ.Level.prop + | Univ0.Level.Coq_lSet -> Univ.Level.set + | Univ0.Level.Level s -> + let s = unquote_string s in + let comps = CString.split '.' s in + let last, dp = CList.sep_last comps in + let dp = DirPath.make (List.map Id.of_string comps) in + let idx = int_of_string last in + Univ.Level.make dp idx + | Univ0.Level.Var n -> Univ.Level.var (unquote_int n) + + let unquote_level_expr (trm : Univ0.Level.t) (b : quoted_bool) : Univ.Universe.t = + let l = unquote_level trm in + let u = Univ.Universe.make l in + if b then Univ.Universe.super u + else u + + let unquote_universe evd (trm : Univ0.Universe.t) = + match trm with + | [] -> Evd.new_univ_variable (Evd.UnivFlexible false) evd + | (l,b)::q -> + evd, List.fold_left (fun u (l,b) -> + let u' = unquote_level_expr l b in Univ.Universe.sup u u') + (unquote_level_expr l b) q + + let print_term (u: t) : Pp.std_ppcmds = failwith "not yet implemented" + end + + module TemplateASTReifier = Reify(TemplateASTQuoter) include TemplateASTReifier diff --git a/test-suite/demo.v b/test-suite/demo.v index c0f64ffd3..8c6580215 100644 --- a/test-suite/demo.v +++ b/test-suite/demo.v @@ -69,9 +69,11 @@ Quote Definition eo_syntax := Eval compute in even. Quote Definition add'_syntax := Eval compute in add'. + (** Reflecting definitions **) -Make Definition zero_from_syntax := (Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0). +Make Definition zero_from_syntax := (Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0 []). +(* the function unquote_kn in reify.ml4 is not yet implemented *) Make Definition add_from_syntax := ltac:(let t:= eval compute in add_syntax in exact t). Make Definition eo_from_syntax := @@ -136,7 +138,6 @@ Definition mut_i : mutual_inductive_entry := mind_entry_finite := Finite; mind_entry_params := []; mind_entry_inds := [one_i; one_i2]; - mind_entry_polymorphic := false; mind_entry_universes := Monomorphic_ctx ([], Constraint.empty); mind_entry_private := None; |}. @@ -164,7 +165,6 @@ Definition mut_list_i : mutual_inductive_entry := mind_entry_finite := Finite; mind_entry_params := [("A", LocalAssum (tSort Universe.type0))]; mind_entry_inds := [one_list_i]; - mind_entry_polymorphic := false; mind_entry_universes := Monomorphic_ctx ([], Constraint.empty); mind_entry_private := None; |}. @@ -190,7 +190,6 @@ Definition mut_pt_i : mutual_inductive_entry := mind_entry_finite := BiFinite; mind_entry_params := [("A", LocalAssum (tSort Universe.type0))]; mind_entry_inds := [one_pt_i]; - mind_entry_polymorphic := false; mind_entry_universes := Monomorphic_ctx ([], Constraint.empty); mind_entry_private := None; |}. @@ -371,7 +370,6 @@ Make Definition myProp := (tSort [(Level.lProp, false)]). Make Definition myProp' := Eval compute in (tSort Universe.type0m). Make Definition mySucProp := (tSort [(Level.lProp, true)]). Make Definition mySet := (tSort [(Level.lSet, false)]). -Print Universes. (** Cofixpoints *) CoInductive streamn : Set := diff --git a/test-suite/univ.v b/test-suite/univ.v index 95d509547..488be5a32 100644 --- a/test-suite/univ.v +++ b/test-suite/univ.v @@ -8,7 +8,7 @@ Set Printing Universes. Inductive foo (A : Type) : Type := | fooc : list A -> foo A. -Print Universes. +(* Print Universes.*) (* Top.1 <= Coq.Init.Datatypes.44 *) Quote Recursively Definition qfoo := foo. @@ -17,10 +17,10 @@ Compute qfoo. Polymorphic Inductive foo2 (A : Type) : Type := | fooc2 : list A -> foo2 A. (* Top.4 |= Top.4 <= Coq.Init.Datatypes.44 *) -Print Universes. +(* Print Universes.*) Definition foo2_instance := foo2. -Print Universes. +(* Print Universes.*) (* Top.9 <= Coq.Init.Datatypes.44 *) Quote Recursively Definition qfoo2 := foo2. @@ -75,7 +75,7 @@ Monomorphic Universe i j. Definition test := (fun (T : Type@{i}) (T2 : Type@{j}) => T -> T2). Set Printing Universes. Print test. -Print Universes. +(* Print Universes. *) Unset Printing Universes. Quote Definition qtest := Eval compute in (fun (T : Type@{i}) (T2 : Type@{j}) => T -> T2). @@ -87,7 +87,7 @@ Make Definition bla' := (tLambda (nNamed "T") (tSort ((Level.Level "Top.2", fals Set Printing Universes. Print bla. Print bla'. -Print Universes. +(* Print Universes. *) Unset Printing Universes. Set Universe Polymorphism. @@ -131,4 +131,4 @@ Make Definition t2 := (Ast.tLambda (Ast.nNamed "T") (Ast.tSort [(Level.Level "To (Ast.tLambda (Ast.nNamed "T2") (Ast.tSort [(Level.Level "Top.10002", false)]) (Ast.tProd Ast.nAnon (Ast.tRel 1) (Ast.tRel 1)))). Set Printing Universes. Print t2. -Print Universes. +(* Print Universes. *) diff --git a/theories/Ast.v b/theories/Ast.v index fbe758c0e..3467fa630 100644 --- a/theories/Ast.v +++ b/theories/Ast.v @@ -112,14 +112,14 @@ Inductive recursivity_kind := Record definition_entry := { definition_entry_type : term; definition_entry_body : term; - definition_entry_polymorphic : bool; definition_entry_universes : universe_context; definition_entry_opaque : bool; }. -Record parameter_entry : Set := { - parameter_entry_type : term }. +Record parameter_entry := { + parameter_entry_type : term; + parameter_entry_universes : universe_context }. Inductive constant_entry := | ParameterEntry (p : parameter_entry) @@ -130,7 +130,6 @@ Record mutual_inductive_entry := { mind_entry_finite : recursivity_kind; mind_entry_params : list (ident * local_entry); mind_entry_inds : list one_inductive_entry; - mind_entry_polymorphic : bool; mind_entry_universes : universe_context; mind_entry_private : option bool }. diff --git a/theories/AstUtils.v b/theories/AstUtils.v index a90b66b64..d8e869113 100644 --- a/theories/AstUtils.v +++ b/theories/AstUtils.v @@ -71,7 +71,6 @@ Proof. mind_entry_finite := Finite; (* inductive *) mind_entry_params := _; mind_entry_inds := _; - mind_entry_polymorphic := _; mind_entry_universes := decl.(ind_universes); mind_entry_private := None |}. - refine (match List.hd_error decl.(ind_bodies) with @@ -96,12 +95,4 @@ Proof. refine (List.map (fun x => fst (fst x)) ind_ctors). refine (List.map (fun x => remove_arity decl.(ind_npars) (snd (fst x))) ind_ctors). - - refine (let '(levels, constraints) := uGraph.repr decl.(ind_universes) in - let not_var := fun l => match l with - | Level.Var _ => false - | _ => true - end in - List.forallb not_var levels - && Constraint.for_all (fun '((l, _), l') => not_var l && not_var l') - constraints). Defined. diff --git a/theories/kernel/univ.v b/theories/kernel/univ.v index 193b8d9a1..a1cd4ee76 100644 --- a/theories/kernel/univ.v +++ b/theories/kernel/univ.v @@ -101,7 +101,7 @@ End Level. Require FSets.FSetWeakList. Require FSets.FMapWeakList. Module LevelDecidableType. - Definition t : Type := Level.t. + Definition t : Set := Level.t. Definition eq : t -> t -> Prop := eq. Definition eq_refl : forall x : t, eq x x := @eq_refl _. Definition eq_sym : forall x y : t, eq x y -> eq y x := @eq_sym _. @@ -276,7 +276,7 @@ Definition make_univ_constraint : universe_level -> constraint_type -> universe_ Require MSets.MSetWeakList. Module ConstraintTypeDec. - Definition t := univ_constraint. + Definition t : Set := univ_constraint. Definition eq : t -> t -> Prop := eq. Definition eq_equiv : RelationClasses.Equivalence eq := _. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. @@ -285,7 +285,9 @@ Module ConstraintTypeDec. End ConstraintTypeDec. Module Constraint := MSets.MSetWeakList.Make ConstraintTypeDec. -Definition constraints := Constraint.t. (* list univ_constraint *) +(** Needs to be in Type because template polymorphism of MSets does not allow setting + the lowest universe *) +Definition constraints : Type := Constraint.t. (* list univ_constraint *) (* val empty_constraint : constraints *) (* val union_constraint : constraints -> constraints -> constraints *) @@ -322,7 +324,7 @@ Definition constraint_function A : Type := A -> A -> constraints -> constraints. Module Instance. - Definition t := list Level.t. + Definition t : Set := list Level.t. (** A universe instance represents a vector of argument universes to a polymorphic definition (constant, inductive or constructor). *) diff --git a/translations/tsl_param.v b/translations/tsl_param.v index 82c2822ff..447ef7422 100644 --- a/translations/tsl_param.v +++ b/translations/tsl_param.v @@ -1,305 +1,297 @@ +(* -*- coq-prog-args: ("-type-in-type" "-top" "Translations.tsl_param") -*- *) Require Import Template.All. -Require Import Arith.Compare_dec. -From Translations Require Import translation_utils. -Import String List Lists.List.ListNotations MonadNotation. -Open Scope list_scope. -Open Scope string_scope. +From Translations Require Import translation_utils sigma. +Import String Lists.List.ListNotations MonadNotation. +Open Scope list_scope. Open Scope string_scope. Open Scope sigma_scope. -Infix "<=" := Nat.leb. -Definition default_term := tVar "constant_not_found". -Definition debug_term msg:= tVar ("debug: " ++ msg). +Reserved Notation "'tsl_ty_param'". -Fixpoint tsl_rec0 (n : nat) (t : term) {struct t} : term := +Fixpoint refresh_universes (t : term) {struct t} := match t with - | tRel k => if n <= k then tRel (2*k-n+1) else t - | tEvar k ts => tEvar k (map (tsl_rec0 n) ts) - | tCast t c a => tCast (tsl_rec0 n t) c (tsl_rec0 n a) - | tProd na A B => tProd na (tsl_rec0 n A) (tsl_rec0 (n+1) B) - | tLambda na A t => tLambda na (tsl_rec0 n A) (tsl_rec0 (n+1) t) - | tLetIn na t A u => tLetIn na (tsl_rec0 n t) (tsl_rec0 n A) (tsl_rec0 (n+1) u) - | tApp t lu => tApp (tsl_rec0 n t) (map (tsl_rec0 n) lu) - | tCase ik t u br => tCase ik (tsl_rec0 n t) (tsl_rec0 n u) - (map (fun x => (fst x, tsl_rec0 n (snd x))) br) - | tProj p t => tProj p (tsl_rec0 n t) - (* | tFix : mfixpoint term -> nat -> term *) - (* | tCoFix : mfixpoint term -> nat -> term *) + | tSort s => tSort [] + | tProd na b t => tProd na b (refresh_universes t) + | tLetIn na b t' t => tLetIn na b t' (refresh_universes t) | _ => t end. -Fixpoint tsl_rec1_app (app : option term) (E : tsl_table) (t : term) : term := - let tsl_rec1 := tsl_rec1_app None in - let debug case symbol := - debug_term ("tsl_rec1: " ++ case ++ " " ++ symbol ++ " not found") in +(* if b it is the first translation, else the second *) +Fixpoint tsl_rec (fuel : nat) (Σ : global_context) (E : tsl_table) (Γ : context) (b : bool) (t : term) {struct fuel} + : tsl_result term := + match fuel with + | O => raise NotEnoughFuel + | S fuel => match t with - | tLambda na A t => - let A0 := tsl_rec0 0 A in - let A1 := tsl_rec1_app None E A in - tLambda na A0 (tLambda (tsl_name tsl_ident na) - (subst_app (lift0 1 A1) [tRel 0]) - (tsl_rec1_app (option_map (lift 2 2) app) E t)) - | t => let t1 := + | tRel n => ret (proj b (tRel n)) + | tSort s => if b then ret (tSort s) + else ret (tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))) + | tCast t c A => if b then + t1 <- tsl_rec fuel Σ E Γ true t ;; + A1 <- tsl_rec fuel Σ E Γ true A ;; + ret (tCast t1 c A1) + else + t1 <- tsl_rec fuel Σ E Γ true t ;; + t2 <- tsl_rec fuel Σ E Γ false t ;; + A2 <- tsl_rec fuel Σ E Γ false A ;; + ret (tCast t2 c (tApp A2 [t1])) + | tProd n A B => if b then + A' <- tsl_ty_param fuel Σ E Γ A ;; + B1 <- tsl_rec fuel Σ E (Γ ,, vass n A) true B ;; + ret (tProd n A' B1) + else + A' <- tsl_ty_param fuel Σ E Γ A ;; + B1 <- tsl_rec fuel Σ E (Γ ,, vass n A) true B ;; + B2 <- tsl_rec fuel Σ E (Γ ,, vass n A) false B ;; + ret (tLambda (nNamed "f") (tProd n A' B1) + (tProd n (lift 1 0 A') + (tApp (lift 1 1 B2) + [tApp (tRel 1) [tRel 0]]))) + | tLambda n A t => A' <- tsl_ty_param fuel Σ E Γ A ;; + t' <- tsl_rec fuel Σ E (Γ ,, vass n A) b t ;; + ret (tLambda n A' t') + | tLetIn n t A u => t' <- tsl_term fuel Σ E Γ t ;; + A' <- tsl_ty_param fuel Σ E Γ A ;; + u' <- tsl_rec fuel Σ E (Γ ,, vdef n t A) b u ;; + ret (tLetIn n t' A' u') + | tApp t u => t' <- tsl_rec fuel Σ E Γ b t ;; + u' <- monad_map (tsl_term fuel Σ E Γ) u ;; + ret (tApp t' u') + | tConst _ _ as t + | tInd _ _ as t + | tConstruct _ _ _ as t => t' <- tsl_term fuel Σ E Γ t ;; + ret (proj b t') + | _ => raise TranslationNotHandeled + end + end +with tsl_term (fuel : nat) (Σ : global_context) (E : tsl_table) (Γ : context) (t : term) {struct fuel} + : tsl_result term := + match fuel with + | O => raise NotEnoughFuel + | S fuel => match t with - | tRel k => tRel (2 * k) - | tSort s => tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s)) - - | tProd na A B => - let A0 := tsl_rec0 0 A in - let A1 := tsl_rec1 E A in - let B0 := tsl_rec0 1 B in - let B1 := tsl_rec1 E B in - let ΠAB0 := tProd na A0 B0 in - tLambda (nNamed "f") ΠAB0 - (tProd na (lift0 1 A0) - (tProd (tsl_name tsl_ident na) - (subst_app (lift0 2 A1) [tRel 0]) - (subst_app (lift 1 2 B1) - [tApp (tRel 2) [tRel 1]]))) - | tApp t us => - let us' := concat (map (fun v => [tsl_rec0 0 v; tsl_rec1 E v]) us) in - mkApps (tsl_rec1 E t) us' - - | tLetIn na t A u => - let t0 := tsl_rec0 0 t in - let t1 := tsl_rec1 E t in - let A0 := tsl_rec0 0 A in - let A1 := tsl_rec1 E A in - let u0 := tsl_rec0 0 u in - let u1 := tsl_rec1 E u in - tLetIn na t0 A0 (tLetIn (tsl_name tsl_ident na) (lift0 1 t1) - (subst_app (lift0 1 A1) [tRel 0]) u1) - - | tCast t c A => let t0 := tsl_rec0 0 t in - let t1 := tsl_rec1 E t in - let A0 := tsl_rec0 0 A in - let A1 := tsl_rec1 E A in - tCast t1 c (mkApps A1 [tCast t0 c A0]) (* apply_subst ? *) - + | tRel n => ret (tRel n) + | tCast t c A => t' <- tsl_term fuel Σ E Γ t ;; + A' <- tsl_ty_param fuel Σ E Γ A ;; + ret (tCast t' c A') | tConst s univs => match lookup_tsl_table E (ConstRef s) with - | Some t => t - | None => debug "tConst" s + | Some t => ret t + | None => raise (TranslationNotFound s) end | tInd i univs => match lookup_tsl_table E (IndRef i) with - | Some t => t - | None => debug "tInd" (match i with mkInd s _ => s end) + | Some t => ret t + | None => raise (TranslationNotFound (string_of_gref (IndRef i))) end | tConstruct i n univs => match lookup_tsl_table E (ConstructRef i n) with - | Some t => t - | None => debug "tConstruct" (match i with mkInd s _ => s end) - end - | tCase ik t u brs as case => - let brs' := List.map (on_snd (lift0 1)) brs in - let case1 := tCase ik (lift0 1 t) (tRel 0) brs' in - match lookup_tsl_table E (IndRef (fst ik)) with - | Some (tInd i _univ) => - tCase (i, (snd ik) * 2) - (tsl_rec1_app (Some (tsl_rec0 0 case1)) E t) - (tsl_rec1 E u) - (map (on_snd (tsl_rec1 E)) brs) - | _ => debug "tCase" (match (fst ik) with mkInd s _ => s end) + | Some t => ret t + | None => raise (TranslationNotFound (string_of_gref (ConstructRef i n))) end - | _ => todo - end in - match app with Some t' => mkApp t1 (t' {3 := tRel 1} {2 := tRel 0}) - | None => t1 end - end. -Definition tsl_rec1 := tsl_rec1_app None. - -Definition tsl_mind_decl (E : tsl_table) - (kn kn' : kername) (mind : minductive_decl) : tsl_table * list minductive_decl. - refine (_, [{| ind_npars := 2 * mind.(ind_npars); - ind_bodies := _; - ind_universes := mind.(ind_universes)|}]). (* FIXME always ok? *) - - refine (fold_left_i (fun E i ind => _ :: _ ++ E)%list mind.(ind_bodies) []). - + (* ind *) - exact (IndRef (mkInd kn i), tInd (mkInd kn' i) []). - + (* ctors *) - refine (fold_left_i (fun E k _ => _ :: E) ind.(ind_ctors) []). - exact (ConstructRef (mkInd kn i) k, tConstruct (mkInd kn' i) k []). - - refine (map_i _ mind.(ind_bodies)). - intros i ind. - refine {| ind_name := tsl_ident ind.(ind_name); - ind_type := _; - ind_kelim := ind.(ind_kelim); - ind_ctors := _; - ind_projs := [] |}. (* todo *) - + (* arity *) - refine (let ar := subst_app (tsl_rec1 E ind.(ind_type)) - [tInd (mkInd kn i) []] in - ar). - + (* constructors *) - refine (map_i _ ind.(ind_ctors)). - intros k ((name, typ), nargs). - refine (tsl_ident name, _, 2 * nargs). - refine (subst_app _ [tConstruct (mkInd kn i) k []]). - refine (fold_left_i (fun t0 i u => t0 {S i := u}) _ (tsl_rec1 E typ)). - (* [I_n-1; ... I_0] *) - refine (rev (map_i (fun i _ => tInd (mkInd kn i) []) - mind.(ind_bodies))). -Defined. - - -Run TemplateProgram (tm <- tmQuote (forall A, A -> A) ;; - let tm' := tsl_rec1 [] tm in - tmUnquote tm' >>= tmPrint). - -Run TemplateProgram (tm <- tmQuote (fun A (x : A) => x) ;; - let tm' := tsl_rec1 [] tm in - tmUnquote tm' >>= tmPrint). - -Goal ((fun f : forall A : Type, A -> A => - forall (A : Type) (A0 : A -> Type) (H : A), A0 H -> A0 (f A H)) (fun A (x : A) => x) - = (forall (A : Type) (A0 : A -> Type) (x : A), A0 x -> A0 x)). -reflexivity. -Defined. - - -Instance param : Translation := - {| tsl_id := tsl_ident ; - tsl_tm := fun ΣE t => ret (tsl_rec1 (snd ΣE) t) ; - tsl_ty := fun '(Σ, E) t => todo "not meaningful here" ; - tsl_ind := fun ΣE kn kn' mind => ret (tsl_mind_decl (snd ΣE) kn kn' mind) |}. - - -Definition T := forall A, A -> A. -Run TemplateProgram (tTranslate emptyTC "T"). - - -Definition tm := ((fun A (x:A) => x) (Type -> Type) (fun x => x)). -Run TemplateProgram (tTranslate emptyTC "tm"). - -Run TemplateProgram (TC <- tTranslate emptyTC "nat" ;; - tmDefinition "nat_TC" TC ). - -Run TemplateProgram (tTranslate nat_TC "pred"). - + | t => match infer Σ Γ t with + | Checked typ => let typ := refresh_universes typ in + t1 <- tsl_rec fuel Σ E Γ true t ;; + t2 <- tsl_rec fuel Σ E Γ false t ;; + typ1 <- tsl_rec fuel Σ E Γ true typ ;; + typ2 <- tsl_rec fuel Σ E Γ false typ ;; + ret (pair typ1 typ2 t1 t2) + | TypeError t => raise (TypingError t) + end + end + end +where "'tsl_ty_param'" := (fun fuel Σ E Γ t => + t1 <- tsl_rec fuel Σ E Γ true t ;; + t2 <- tsl_rec fuel Σ E Γ false t ;; + ret (pack t1 t2)). -Module Id1. - Definition ID := forall A, A -> A. - Run TemplateProgram (tTranslate emptyTC "ID"). - Lemma param_ID_identity (f : ID) - : IDᵗ f -> forall A x, f A x = x. - Proof. - compute. intros H A x. - exact (H A (fun y => y = x) x (eq_refl x)). - Qed. +Instance tsl_param : Translation + := {| tsl_id := tsl_ident ; + tsl_tm := fun ΣE => tsl_term fuel (fst ΣE) (snd ΣE) [] ; + tsl_ty := fun ΣE => tsl_ty_param fuel (fst ΣE) (snd ΣE) [] ; + tsl_ind := todo |}. - Definition toto := fun n : nat => (fun y => 0) (fun _ : Type => n). - Run TemplateProgram (tTranslate nat_TC "toto"). +Definition TslParam := @tTranslate tsl_param. +Definition ImplParam := @tImplement tsl_param. - Definition my_id : ID := - let n := 12 in (fun (_ : nat) y => y) 4 (fun A x => (fun _ : nat => x) n). - Run TemplateProgram (tTranslate nat_TC "my_id"). +Notation "'TYPE'" := (exists A, A -> Type). +Notation "'El' A" := (sigma (π1 A) (π2 A)) (at level 20). +Definition Ty := Type. +Set Printing Universes. +Run TemplateProgram (TslParam emptyTC "Ty"). +Check Tyᵗ : El Tyᵗ. - Definition free_thm_my_id : forall A x, my_id A x = x - := param_ID_identity my_id my_idᵗ. -End Id1. +Definition mkTYPE (A₀ : Type) (Aᴿ : A₀ -> Type) : El Tyᵗ := + @mk_sig Type (fun A₀ => A₀ -> Type) A₀ Aᴿ. -Module Id2. - Definition ID := forall A x y (p : x = y :> A), x = y. +Definition Prodᶠ (A : El Tyᵗ) (B : El A -> El Tyᵗ) : El Tyᵗ := + mkTYPE + (forall x : El A, (B x).1) + (fun f₀ => forall x : El A, (B x).2 (f₀ x)). - Run TemplateProgram (TC <- tTranslate emptyTC "eq" ;; - TC <- tTranslate TC "ID" ;; - tmDefinition "TC" TC). +Notation "A →ᶠ B" := (Prodᶠ A (fun _ => B)) (at level 99, right associativity, B at level 200). +Notation "'Πᶠ' x .. y , P" := (Prodᶠ _ (fun x => .. (Prodᶠ _ (fun y => P)) ..)) + (at level 200, x binder, y binder, right associativity). +Definition Lamᶠ {A : El Tyᵗ} {B : El A -> El Tyᵗ} (f : forall x : El A, El (B x)) : El (Prodᶠ A B). +Proof. +unshelve refine (_ ; _). ++ refine (fun x => (f x).1). ++ refine (fun x => (f x).2). +Defined. - Lemma param_ID_identity (f : ID) - : IDᵗ f -> forall A x y p, f A x y p = p. - Proof. - compute. intros H A x y p. - destruct p. - specialize (H A (fun y => x = y) x eq_refl x eq_refl eq_refl - (eq_reflᵗ _ _ _ _)). - destruct H. reflexivity. - Qed. - - Definition myf : ID - := fun A x y p => eq_trans (eq_trans p (eq_sym p)) p. - - Run TemplateProgram (TC <- tTranslate TC "eq_sym" ;; - TC <- tTranslate TC "eq_trans" ;; - tTranslate TC "myf"). - - Definition free_thm_myf : forall A x y p, myf A x y p = p - := param_ID_identity myf myfᵗ. -End Id2. - +Notation "'λᶠ' x .. y , t" := (Lamᶠ (fun x => .. (Lamᶠ (fun y => t)) ..)) + (at level 200, x binder, y binder, right associativity). +Definition Appᶠ {A B} (f : El (Prodᶠ A B)) (x : El A) : El (B x). +Proof. +unshelve refine (_ ; _). ++ refine (f.1 x). ++ refine (f.2 x). +Defined. +Notation "t · u" := (Appᶠ t u) (at level 65, left associativity). -Module Vectors. - Import Vector. - Run TemplateProgram (tTranslate nat_TC "t"). -End Vectors. +Definition sigmaᵀ (A : El Tyᵗ) (P : El (A →ᶠ Tyᵗ)) : Type := + sigma (El A) (fun x => El (P · x)). -Require Import Even. -Run TemplateProgram (tTranslate nat_TC "even"). +Definition existᵀ (A : El Tyᵗ) (P : El (A →ᶠ Tyᵗ)) + (x : El A) (y : El (P · x)) : sigmaᵀ A P + := mk_sig x y. -Definition rev_type := forall A, list A -> list A. -Run TemplateProgram (TC <- tTranslate emptyTC "list" ;; - TC <- tTranslate TC "rev_type" ;; - tmDefinition "list_TC" TC ). +Inductive sigmaᴿ (A : El Tyᵗ) (P : El (A →ᶠ Tyᵗ)) : sigmaᵀ A P -> Type := +| existᴿ : forall (x : El A) (y : El (P · x)), sigmaᴿ A P (existᵀ A P x y). +Definition sigmaᶠ : El (Πᶠ (A : El Tyᵗ) (P : El (A →ᶠ Tyᵗ)), Tyᵗ). +Proof. +refine (λᶠ A P, _). +unshelve refine (mkTYPE _ (sigmaᴿ A P)). +Defined. +Definition existᶠ : El (Πᶠ (A : El Tyᵗ) (P : El (A →ᶠ Tyᵗ)) (x : El A) (y : El (P · x)), + sigmaᶠ · A · P). +Proof. +refine (λᶠ A P x y, _). +refine (mk_sig (existᵀ A P x y) (existᴿ A P x y)). +Defined. -(* Definition isequiv (A B : Type) (f : A -> B) := *) -(* exists (g : B -> A), (forall x, g (f x) = x) × (forall y, f (g y) = y). *) +Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. -(* Definition equiv_id A : isequiv A A (fun x => x). *) -(* unshelve econstructor. exact (fun y => y). *) -(* split; reflexivity. *) -(* Defined. *) +Inductive eq2 (A : El Tyᵗ) (x : El A) : + forall (y : El A), eq (π1 x) (π1 y) -> Prop := +| refl2 : eq2 A x x (eq_refl _). -(* Run TemplateProgram (TC <- tTranslate [] "sigma" ;; *) -(* TC <- tTranslate TC "eq" ;; *) -(* TC <- tTranslate TC "isequiv" ;; *) -(* TC <- tTranslate TC "equiv_id" ;; *) -(* tmDefinition "TC" TC). *) -(* Quote Definition eq_rect_Type_ := (forall (A : Type) (x : A) (P : A -> Type), *) -(* P x -> forall y : A, x = y -> P y). *) -(* Make Definition eq_rect_Typeᵗ := ltac:(let t:= eval compute in (tsl_rec1 TC eq_rect_Type_) in exact t). *) +Definition eqᶠ : El (Πᶠ (A : El Tyᵗ), A →ᶠ A →ᶠ Tyᵗ). +Proof. +refine (λᶠ A x y, _). +unshelve refine (mkTYPE _ _). ++ refine (eq x.1 y.1). ++ refine (eq2 A x y). +Defined. -(* Lemma eq_rectᵗ : eq_rect_Typeᵗ eq_rect. *) -(* compute. intros A Aᵗ x xᵗ P Pᵗ X X0 y yᵗ H H0. *) -(* by destruct H0. *) -(* Defined. *) +Definition reflᶠ : El (Πᶠ (A : El Tyᵗ) (x : El A), eqᶠ · A · x · x). +Proof. +refine (λᶠ A x, _). +unshelve refine (_; refl2 A x). +Defined. -(* Definition TC' := (ConstRef "Coq.Init.Logic.eq_rect", tConst "eq_rectᵗ" []) :: TC. *) +Definition Falseᶠ : El Tyᵗ. + exists False. exact (fun _ => False). +Defined. + + +Quote Recursively Definition sigma_prog := @sigma. +Quote Recursively Definition eq_prog := @eq. +Quote Recursively Definition false_prog := @False. +Definition sigma_decl := Eval compute in + extract_mind_decl_from_program "Translations.sigma.sigma" sigma_prog. +Definition eq_decl := Eval compute in + extract_mind_decl_from_program "Translations.tsl_param.eq" eq_prog. +Definition false_decl := Eval compute in + extract_mind_decl_from_program "Coq.Init.Logic.False" false_prog. + + +Definition ΣE : option tsl_context := + sd <- sigma_decl ;; + ed <- eq_decl ;; + fd <- false_decl ;; + let Σ' := add_global_decl (InductiveDecl "Coq.Init.Logic.False" fd) ( + add_global_decl (InductiveDecl "Translations.tsl_param.eq" ed) ( + add_global_decl (InductiveDecl "Translations.sigma.sigma" sd) + ([], init_graph))) in + let E' := [(IndRef (mkInd "Translations.sigma.sigma" 0), + tConst "sigmaᶠ" []); + (ConstructRef (mkInd "Translations.sigma.sigma" 0) 0, + tConst "existᶠ" []); + (IndRef (mkInd "Translations.tsl_param.eq" 0), tConst "eqᶠ" []); + (IndRef (mkInd "Coq.Init.Logic.False" 0), tConst "Falseᶠ" []) + ] in + ret (Σ', E'). + +Definition HasTwoElFstComponentᵗ : El (Tyᵗ →ᶠ Tyᵗ) + := λᶠ (T : El Tyᵗ), mkTYPE (exists (x y : T.1), x = y -> False) (fun _ => unit). + + +Definition equiv (A B : Type) := + (* Type. *) + exists (f : A -> B) (g : B -> A), + (forall x, eq (g (f x)) x) × (forall x, eq (f (g x)) x). + +Definition FALSE := forall X, X. +Run TemplateProgram (TslParam emptyTC "FALSE"). + +Proposition consistency_preservation : El FALSEᵗ -> FALSE. + compute. + intros [f _] X. + exact (f (X; fun _ => unit)). +Defined. -(* Definition eq_to_iso A B : A = B -> exists f, isequiv A B f. *) -(* refine (eq_rect _ (fun B => exists f : A -> B, isequiv A B f) _ _). *) -(* econstructor. *) -(* eapply equiv_id. *) +Quote Definition equiv_ := Eval compute in equiv. + + +(* Check "go". *) + +(* Run TemplateProgram (match ΣE with *) +(* | None => tmFail "bug: no tsl_ctx" *) +(* | Some ΣE => *) +(* ΣE <- TslParam ΣE "equiv" ;; *) +(* (* tmPrint ΣE' ;; *) *) +(* tmPrint "lo" ;; *) +(* H <- ImplParam ΣE "notUnivalence" *) +(* (exists A B : Type, (equiv A B) × exists P, P A × ((P B) -> False)) ;; *) +(* (* (exists A : Type, (equiv A A)) ;; *) *) +(* tmPrint "done" *) +(* end). *) +(* Check "proof". *) +(* Next Obligation. *) +(* simple refine (existᶠ · _ · _ · _ · _). *) +(* exact (bool:Type; fun _=> unit:Type). *) +(* simple refine (existᶠ · _ · _ · _ · _). *) +(* exact (unit:Type; fun _ => bool:Type). *) +(* simple refine (existᶠ · _ · _ · _ · _). *) +(* - simple refine (existᶠ · _ · _ · _ · _). *) +(* exists π2. exact π1. *) +(* simple refine (existᶠ · _ · _ · _ · _). *) +(* exists π2. exact π1. *) +(* simple refine (existᶠ · _ · _ · _ · _); *) +(* cbn; unshelve econstructor; reflexivity. *) +(* - simple refine (existᶠ · _ · _ · _ · _). *) +(* exact HasTwoElFstComponentᵗ. *) +(* simple refine (existᶠ · _ · _ · _ · _). *) +(* + cbn. refine (_; tt). exists true. exists false. *) +(* discriminate 1. *) +(* + compute. *) +(* split; (intro p; *) +(* destruct p as [p _]; *) +(* destruct p as [[] [[] p]]; *) +(* contradiction p; reflexivity). *) (* Defined. *) -(* Definition UA := forall A B, isequiv _ _ (eq_to_iso A B). *) - -(* Run TemplateProgram (TC <- tTranslate TC' "eq_to_iso" ;; *) -(* tTranslate TC "UA"). *) - -(* Arguments isequiv {A B} _. *) -(* Arguments isequivᵗ {_ _ _ _} _ _. *) -(* Arguments eqᵗ {A Aᵗ x xᵗ H} _ _. *) - -(* Axiom ua : UA. *) - -(* Goal UAᵗ ua. *) -(* intros A Aᵗ B Bᵗ. *) -(* unshelve econstructor. *) -(* - intros [f e] []. clear f e. *) -(* assert (forall H, isequiv (π1ᵗ H)). { *) -(* destruct π2ᵗ. destruct π2ᵗ. *) -(* intro x. unshelve econstructor. *) -(* by refine (fun y => eq_rect _ Aᵗ (π1ᵗ0 _ y) _ _). *) -(* split. { intro. *) +(* Check "ok!". *)