diff options
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 529 |
1 files changed, 298 insertions, 231 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 52179ae5..04006453 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1,7 +1,7 @@ open Printer open Pp open Names -open Term +open Constr open Vars open Glob_term open Glob_ops @@ -12,6 +12,9 @@ open Util open Glob_termops open Misctypes +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let observe strm = if do_observe () then Feedback.msg_debug strm @@ -29,6 +32,14 @@ type binder_type = type glob_context = (binder_type*glob_constr) list + +let rec solve_trivial_holes pat_as_term e = + match DAst.get pat_as_term, DAst.get e with + | GHole _,_ -> e + | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe -> + DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) + | _,_ -> pat_as_term + (* compose_glob_context [(bt_1,n_1,t_1);......] rt returns b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the @@ -39,7 +50,7 @@ let compose_glob_context = match bt with | Lambda n -> mkGLambda(n,t,acc) | Prod n -> mkGProd(n,t,acc) - | LetIn n -> mkGLetIn(n,t,acc) + | LetIn n -> mkGLetIn(n,t,None,acc) in List.fold_right compose_binder @@ -109,13 +120,13 @@ let combine_args arg args = let ids_of_binder = function - | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> [] - | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id] + | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty + | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id let rec change_vars_in_binder mapping = function [] -> [] | (bt,t)::l -> - let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in + let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in (bt,change_vars mapping t):: (if Id.Map.is_empty new_mapping then l @@ -126,27 +137,27 @@ let rec replace_var_by_term_in_binder x_id term = function | [] -> [] | (bt,t)::l -> (bt,replace_var_by_term x_id term t):: - if Id.List.mem x_id (ids_of_binder bt) + if Id.Set.mem x_id (ids_of_binder bt) then l else replace_var_by_term_in_binder x_id term l -let add_bt_names bt = List.append (ids_of_binder bt) +let add_bt_names bt = Id.Set.union (ids_of_binder bt) let apply_args ctxt body args = let need_convert_id avoid id = - List.exists (is_free_in id) args || Id.List.mem id avoid + List.exists (is_free_in id) args || Id.Set.mem id avoid in let need_convert avoid bt = - List.exists (need_convert_id avoid) (ids_of_binder bt) + Id.Set.exists (need_convert_id avoid) (ids_of_binder bt) in - let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = + let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) = match na with - | Name id when Id.List.mem id avoid -> + | Name id when Id.Set.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in - Name new_id,Id.Map.add id new_id mapping,new_id::avoid + Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid | _ -> na,mapping,avoid in - let next_bt_away bt (avoid:Id.t list) = + let next_bt_away bt (avoid:Id.Set.t) = match bt with | LetIn na -> let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in @@ -171,15 +182,15 @@ let apply_args ctxt body args = let new_avoid,new_ctxt',new_body,new_id = if need_convert_id avoid id then - let new_avoid = id::avoid in + let new_avoid = Id.Set.add id avoid in let new_id = Namegen.next_ident_away id new_avoid in - let new_avoid' = new_id :: new_avoid in + let new_avoid' = Id.Set.add new_id new_avoid in let mapping = Id.Map.add id new_id Id.Map.empty in let new_ctxt' = change_vars_in_binder mapping ctxt' in let new_body = change_vars mapping body in new_avoid',new_ctxt',new_body,new_id else - id::avoid,ctxt',body,id + Id.Set.add id avoid,ctxt',body,id in let new_body = replace_var_by_term new_id arg new_body in let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in @@ -203,7 +214,7 @@ let apply_args ctxt body args = in (new_bt,t)::new_ctxt',new_body in - do_apply [] ctxt body args + do_apply Id.Set.empty ctxt body args let combine_app f args = @@ -223,7 +234,12 @@ let combine_lam n t b = compose_glob_context b.context b.value ) } - +let combine_prod2 n t b = + { + context = []; + value = mkGProd(n, compose_glob_context t.context t.value, + compose_glob_context b.context b.value ) + } let combine_prod n t b = { context = t.context@((Prod n,t.value)::b.context); value = b.value} @@ -245,10 +261,10 @@ let mk_result ctxt value avoid = **************************************************) let coq_True_ref = - lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True") + lazy (Coqlib.coq_reference "" ["Init";"Logic"] "True") let coq_False_ref = - lazy (Coqlib.gen_reference "" ["Init";"Logic"] "False") + lazy (Coqlib.coq_reference "" ["Init";"Logic"] "False") (* [make_discr_match_el \[e1,...en\]] builds match e1,...,en with @@ -271,10 +287,10 @@ let make_discr_match_el = *) let make_discr_match_brl i = List.map_i - (fun j (_,idl,patl,_) -> + (fun j {CAst.v=(idl,patl,_)} -> CAst.make @@ if Int.equal j i - then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref)) - else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref)) + then (idl,patl, mkGRef (Lazy.force coq_True_ref)) + else (idl,patl, mkGRef (Lazy.force coq_False_ref)) ) 0 (* @@ -333,27 +349,28 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in - let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in - let open Context.Named.Declaration in - Environ.push_named (of_tuple (id,value,typ)) env + let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + (match raw_value with + | None -> + EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env + | Some value -> + EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env) let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = - let open Context.Rel.Declaration in observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); - match pat with - | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,typ)) env - | PatCstr(_,c,patl,na) -> + match DAst.get pat with + | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env + | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env (Evd.from_env env) typ + try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in - let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) in let new_env = add_pat_variables env pat typ in @@ -361,21 +378,30 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let _,v,t = Context.Rel.Declaration.to_tuple decl in - match Context.Rel.Declaration.get_name decl with - | Anonymous -> assert false - | Name id -> - let new_t = substl ctxt t in - let new_v = Option.map (substl ctxt) v in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ - Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) - ); - let open Context.Named.Declaration in - (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt) - ) + let open Context.Rel.Declaration in + let sigma, _ = Pfedit.get_current_context () in + match decl with + | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false + | LocalAssum (Name id, t) -> + let new_t = substl ctxt t in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) + | LocalDef (Name id, v, t) -> + let new_t = substl ctxt t in + let new_v = substl ctxt v in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++ + str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++ + str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) + ) (Environ.rel_context new_env) ~init:(env,[]) ) @@ -386,31 +412,30 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = function - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> +let rec pattern_to_term_and_type env typ = DAst.with_val (function + | PatVar Anonymous -> assert false + | PatVar (Name id) -> mkGVar id - | PatCstr(loc,constr,patternl,_) -> + | PatCstr(constr,patternl,_) -> let cst_narg = Inductiveops.constructor_nallargs_env (Global.env ()) constr in let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env (Evd.from_env env) typ + try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in - let open Context.Rel.Declaration in - let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in let implicit_args = Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i)) + (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i))) ) in let patl_as_term = @@ -419,6 +444,7 @@ let rec pattern_to_term_and_type env typ = function mkGApp(mkGRef(ConstructRef constr), implicit_args@patl_as_term ) + ) (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the @@ -452,13 +478,14 @@ let rec pattern_to_term_and_type env typ = function *) -let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr rt); - match rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> +let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = + observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); + let open CAst in + match DAst.get rt with + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid - | GApp(_,_,_) -> + | GApp(_,_) -> let f,args = glob_decompose_app rt in let args_res : (glob_constr list) build_entry_return = List.fold_right (* create the arguments lists of constructors and combine them *) @@ -470,20 +497,20 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = (mk_result [] [] avoid) in begin - match f with + match DAst.get f with | GLambda _ -> let rec aux t l = match l with | [] -> t - | u::l -> - match t with - | GLambda(loc,na,_,nat,b) -> - GLetIn(Loc.ghost,na,u,aux b l) + | u::l -> DAst.make @@ + match DAst.get t with + | GLambda(na,_,nat,b) -> + GLetIn(na,u,None,aux b l) | _ -> - GApp(Loc.ghost,t,l) + GApp(t,l) in build_entry_lc env funnames avoid (aux f args) - | GVar(_,id) when Id.Set.mem id funnames -> + | GVar id when Id.Set.mem id funnames -> (* if we have [f t1 ... tn] with [f]$\in$[fnames] then we create a fresh variable [res], add [res] and its "value" (i.e. [res v1 ... vn]) to each @@ -492,8 +519,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = The "value" of this branch is then simply [res] *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in - let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in - let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in + let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in + let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in @@ -524,7 +551,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = args_res.result } | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) - | GLetIn(_,n,t,b) -> + | GLetIn(n,v,t,b) -> (* if we have [(let x := v in b) t1 ... tn] , we discard our work and compute the list of constructor for [let x = v in (b t1 ... tn)] up to alpha conversion @@ -533,12 +560,12 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = match n with | Name id when List.exists (is_free_in id) args -> (* need to alpha-convert the name *) - let new_id = Namegen.next_ident_away id avoid in + let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in let new_avoid = id:: avoid in let new_b = replace_var_by_term id - (GVar(Loc.ghost,id)) + (DAst.make @@ GVar id) b in (Name new_id,new_b,new_avoid) @@ -548,7 +575,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = env funnames avoid - (mkGLetIn(new_n,t,mkGApp(new_b,args))) + (mkGLetIn(new_n,v,t,mkGApp(new_b,args))) | GCases _ | GIf _ | GLetTuple _ -> (* we have [(match e1, ...., en with ..... end) t1 tn] we first compute the result from the case and @@ -556,18 +583,18 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let f_res = build_entry_lc env funnames args_res.to_avoid f in combine_results combine_app f_res args_res - | GCast(_,b,_) -> + | GCast(b,_) -> (* for an applied cast we just trash the cast part and restart the work. WARNING: We need to restart since [b] itself should be an application term *) build_entry_lc env funnames avoid (mkGApp(b,args)) - | GRec _ -> error "Not handled GRec" - | GProd _ -> error "Cannot apply a type" + | GRec _ -> user_err Pp.(str "Not handled GRec") + | GProd _ -> user_err Pp.(str "Cannot apply a type") end (* end of the application treatement *) - | GLambda(_,n,_,t,b) -> + | GLambda(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -582,7 +609,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (new_n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_lam new_n) t_res b_res - | GProd(_,n,_,t,b) -> + | GProd(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -591,45 +618,47 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let t_res = build_entry_lc env funnames avoid t in let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in - combine_results (combine_prod n) t_res b_res - | GLetIn(_,n,v,b) -> + if List.length t_res.result = 1 && List.length b_res.result = 1 + then combine_results (combine_prod2 n) t_res b_res + else combine_results (combine_prod n) t_res b_res + | GLetIn(n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] and combine the two result *) + let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in - let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in + let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = - let open Context.Named.Declaration in match n with Anonymous -> env - | Name id -> Environ.push_named (of_tuple (id,Some v_as_constr,v_type)) env + | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res - | GCases(_,_,_,el,brl) -> + | GCases(_,_,el,brl) -> (* we create the discrimination function and treat the case itself *) let make_discr = make_discr_match brl in build_entry_lc_from_case env funnames make_discr el brl avoid - | GIf(_,b,(na,e_option),lhs,rhs) -> + | GIf(b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in + let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + user_err (str "Cannot find the inductive associated to " ++ + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) [] in assert (Int.equal (Array.length case_pats) 2); let brl = List.map_i - (fun i x -> (Loc.ghost,[],[case_pats.(i)],x)) + (fun i x -> CAst.make ([],[case_pats.(i)],x)) 0 [lhs;rhs] in @@ -638,7 +667,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) build_entry_lc env funnames avoid match_expr - | GLetTuple(_,nal,_,b,e) -> + | GLetTuple(nal,_,b,e) -> begin let nal_as_glob_constr = List.map @@ -649,25 +678,23 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = nal in let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in + let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - errorlabstrm "" (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + user_err (str "Cannot find the inductive associated to " ++ + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); - let br = - (Loc.ghost,[],[case_pats.(0)],e) - in + let br = CAst.make ([],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr end - | GRec _ -> error "Not handled GRec" - | GCast(_,b,_) -> + | GRec _ -> user_err Pp.(str "Not handled GRec") + | GCast(b,_) -> build_entry_lc env funnames avoid b and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) @@ -696,7 +723,7 @@ and build_entry_lc_from_case env funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in - Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr + EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr) ) el in (****** The next works only if the match is not dependent ****) @@ -727,7 +754,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve | [] -> (* computed_branches *) {result = [];to_avoid = avoid} | br::brl' -> (* alpha conversion to prevent name clashes *) - let _,idl,patl,return = alpha_br avoid br in + let {CAst.v=(idl,patl,return)} = alpha_br avoid br in let new_avoid = idl@avoid in (* for now we can no more use idl as an identifier *) (* building a list of precondition stating that we are not in this branch (will be used in the following recursive calls) @@ -743,10 +770,10 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.fold_right (fun id acc -> let typ_of_id = - Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id) + Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype false [] + Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids (Evd.from_env env) typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) @@ -791,15 +818,22 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.map3 (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in - let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in + let typ_as_constr = EConstr.of_constr typ_as_constr in + let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in + (* removing trivial holes *) + let pat_as_term = solve_trivial_holes pat_as_term e in + (* observe (str "those_pattern_preconds" ++ spc () ++ *) + (* str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *) + (* str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *) + (* str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *) List.fold_right (fun id acc -> if Id.Set.mem id this_pat_ids then (Prod (Name id), - let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in + let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype false [] new_env (Evd.from_env env) typ_of_id + Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id in raw_typ_of_id )::acc @@ -841,37 +875,45 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve { brl'_res with result = this_branch_res@brl'_res.result } -let is_res id = - try +let is_res r = match DAst.get r with +| GVar id -> + begin try String.equal (String.sub (Id.to_string id) 0 4) "_res" - with Invalid_argument _ -> false + with Invalid_argument _ -> false end +| _ -> false +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false +let is_gvar c = match DAst.get c with +| GVar id -> true +| _ -> false let same_raw_term rt1 rt2 = - match rt1,rt2 with - | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2 + match DAst.get rt1, DAst.get rt2 with + | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = - let rec decompose_raw_eq lhs rhs acc = - observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs); - let (rhd,lrhs) = glob_decompose_app rhs in - let (lhd,llhs) = glob_decompose_app lhs in - observe (str "lhd := " ++ pr_glob_constr lhd); - observe (str "rhd := " ++ pr_glob_constr rhd); + let _, env = Pfedit.get_current_context () in + let rec decompose_raw_eq lhs rhs acc = + observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs); + let (rhd,lrhs) = glob_decompose_app rhs in + let (lhd,llhs) = glob_decompose_app lhs in + observe (str "lhd := " ++ pr_glob_constr_env env lhd); + observe (str "rhd := " ++ pr_glob_constr_env env rhd); observe (str "llhs := " ++ int (List.length llhs)); observe (str "lrhs := " ++ int (List.length lrhs)); - let sllhs = List.length llhs in - let slrhs = List.length lrhs in - if same_raw_term lhd rhd && Int.equal sllhs slrhs + let sllhs = List.length llhs in + let slrhs = List.length lrhs in + if same_raw_term lhd rhd && Int.equal sllhs slrhs then (* let _ = assert false in *) List.fold_right2 decompose_raw_eq llhs lrhs acc else (lhs,rhs)::acc in decompose_raw_eq lhs rhs [] - exception Continue (* @@ -880,28 +922,30 @@ exception Continue eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_glob_constr rt); + observe (str "rebuilding : " ++ pr_glob_constr_env env rt); let open Context.Rel.Declaration in - match rt with - | GProd(_,n,k,t,b) -> + let open CAst in + match DAst.get rt with + | GProd(n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin - match t with - | GApp(_,(GVar(_,res_id) as res_rt),args') when is_res res_id -> + match DAst.get t with + | GApp(res_rt ,args') when is_res res_rt -> begin - match args' with - | (GVar(_,this_relname))::args' -> + let arg = List.hd args' in + match DAst.get arg with + | GVar this_relname -> (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious i*) let new_t = - mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) + mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt]) in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -913,12 +957,16 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt]) - when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + | GApp(eq_as_ref,[ty; id ;rt]) + when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> + let loc1 = rt.CAst.loc in + let loc2 = eq_as_ref.CAst.loc in + let loc3 = id.CAst.loc in + let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try - observe (str "computing new type for eq : " ++ pr_glob_constr rt); + observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt); let t' = try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) with e when CErrors.noncritical e -> raise Continue @@ -932,7 +980,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let subst_b = if is_in_b then b else replace_var_by_term id rt b in - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env @@ -942,51 +990,50 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in mkGProd(n,t,new_b),id_to_exclude with Continue -> - let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in + let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in - let ind,args' = Inductive.find_inductive env ty' in + let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in let mib,_ = Global.lookup_inductive (fst ind) in let nparam = mib.Declarations.mind_nparams in let params,arg' = ((Util.List.chop nparam args')) in - let rt_typ = - GApp(Loc.ghost, - GRef (Loc.ghost,Globnames.IndRef (fst ind),None), + let rt_typ = DAst.make @@ + GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map - (fun p -> Detyping.detype false [] + (fun p -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) - p) params)@(Array.to_list + (EConstr.of_constr p)) params)@(Array.to_list (Array.make (List.length args' - nparam) (mkGHole ())))) in let eq' = - GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt]) + DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in - observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); + observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; + let sigma = Evd.(from_env env) in let new_args = - match kind_of_term eq'_as_constr with + match EConstr.kind sigma eq'_as_constr with | App(_,[|_;_;ty;_|]) -> - let ty = Array.to_list (snd (destApp ty)) in + let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in let ty' = snd (Util.List.chop nparam ty) in List.fold_left2 (fun acc var_as_constr arg -> if isRel var_as_constr then - let open Context.Rel.Declaration in - let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in + let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in match na with | Anonymous -> acc | Name id' -> - (id',Detyping.detype false [] + (id',Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) arg)::acc else if isVar var_as_constr - then (destVar var_as_constr,Detyping.detype false [] + then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) arg)::acc @@ -1015,7 +1062,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in let new_env = let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in - Environ.push_rel (LocalAssum (n,t')) env + EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons @@ -1031,8 +1078,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2]) - when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + | GApp(eq_as_ref,[ty;rt1;rt2]) + when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin try @@ -1043,7 +1090,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = List.fold_left (fun acc (lhs,rhs) -> mkGProd(Anonymous, - mkGApp(mkGRef(eq_as_ref),[mkGHole ();lhs;rhs]),acc) + mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc) ) b l @@ -1051,9 +1098,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = rebuild_cons env nb_args relname args crossed_types depth new_rt else raise Continue with Continue -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1067,9 +1114,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | _ -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1082,15 +1129,15 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (Id.Set.filter not_free_in_t id_to_exclude) | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end - | GLambda(_,n,k,t,b) -> + | GLambda(n,k,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in - observe (str "computing new type for lambda : " ++ pr_glob_constr rt); + observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1101,18 +1148,21 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude - | _ -> anomaly (Pp.str "Should not have an anonymous function here") + DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude + | _ -> anomaly (Pp.str "Should not have an anonymous function here.") (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | GLetIn(_,n,t,b) -> + | GLetIn(n,v,t,b) -> begin + let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in let evd = Evd.from_ctx ctx in - let type_t' = Typing.unsafe_type_of env evd t' in + let type_t' = Typing.unsafe_type_of env evd t' in + let t' = EConstr.Unsafe.to_constr t' in + let type_t' = EConstr.Unsafe.to_constr type_t' in let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1122,10 +1172,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(Loc.ghost,n,t,new_b), + | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end - | GLetTuple(_,nal,(na,rto),t,b) -> + | GLetTuple(nal,(na,rto),t,b) -> assert (Option.is_empty rto); begin let not_free_in_t id = not (is_free_in id t) in @@ -1137,7 +1187,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = depth t in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = Environ.push_rel (LocalAssum (na,t')) env in + let new_env = EConstr.push_rel (LocalAssum (na,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1148,7 +1198,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Id.Set.mem id id_to_exclude -> *) (* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - GLetTuple(Loc.ghost,nal,(na,None),t,new_b), + DAst.make @@ GLetTuple(nal,(na,None),t,new_b), Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end @@ -1174,31 +1224,39 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) -let rec compute_cst_params relnames params = function +let rec compute_cst_params relnames params gt = DAst.with_val (function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp(_,GVar(_,relname'),rtl) when Id.Set.mem relname' relnames -> - compute_cst_params_from_app [] (params,rtl) - | GApp(_,f,args) -> + | GApp(f,args) -> + begin match DAst.get f with + | GVar relname' when Id.Set.mem relname' relnames -> + compute_cst_params_from_app [] (params,args) + | _ -> List.fold_left (compute_cst_params relnames) params (f::args) - | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> + end + | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b + | GLetIn(_,v,t,b) -> + let v_params = compute_cst_params relnames params v in + let t_params = Option.fold_left (compute_cst_params relnames) v_params t in + compute_cst_params relnames t_params b | GCases _ -> params (* If there is still cases at this point they can only be discrimination ones *) | GSort _ -> params | GHole _ -> params | GIf _ | GRec _ | GCast _ -> - raise (UserError("compute_cst_params", str "Not handled case")) + raise (UserError(Some "compute_cst_params", str "Not handled case")) + ) gt and compute_cst_params_from_app acc (params,rtl) = + let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' - when Id.compare id id' == 0 && not is_defined -> + | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts = +let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1213,11 +1271,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) let _ = try List.iteri - (fun i ((n,nt,is_defined) as param) -> + (fun i ((n,nt,typ) as param) -> if Array.for_all (fun l -> - let (n',nt',is_defined') = List.nth l i in - Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined') + let (n',nt',typ') = List.nth l i in + Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ') rels_params then l := param::!l @@ -1229,18 +1287,18 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) List.rev !l let rec rebuild_return_type rt = - match rt with - | Constrexpr.CProdN(loc,n,t') -> - Constrexpr.CProdN(loc,n,rebuild_return_type t') - | Constrexpr.CLetIn(loc,na,t,t') -> - Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], - Constrexpr.Default Decl_kinds.Explicit,rt], - Constrexpr.CSort(Loc.ghost,GType [])) - + let loc = rt.CAst.loc in + match rt.CAst.v with + | Constrexpr.CProdN(n,t') -> + CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') + | Constrexpr.CLetIn(na,v,t,t') -> + CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], + Constrexpr.Default Decl_kinds.Explicit, rt)], + CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive - evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list) + evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in @@ -1262,36 +1320,41 @@ let do_build_inductive let open Context.Named.Declaration in let evd,env = Array.fold_right2 - (fun id c (evd,env) -> - let evd,t = Typing.type_of env evd (mkConstU c) in + (fun id (c, u) (evd,env) -> + let u = EConstr.EInstance.make u in + let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in + let t = EConstr.Unsafe.to_constr t in evd, Environ.push_named (LocalAssum (id,t)) - (* try *) - (* Typing.e_type_of env evd (mkConstU c) *) - (* with Not_found -> *) - (* raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) *) env ) funnames (Array.of_list funconstants) (evd,Global.env ()) in - let resa = Array.map (build_entry_lc env funnames_as_set []) rta in + (* we solve and replace the implicits *) + let rta = + Array.mapi (fun i rt -> + let _,t = Typing.type_of env evd (EConstr.of_constr (mkConstU ((Array.of_list funconstants).(i)))) in + resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt + ) rta + in + let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = funargs in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + (fun (n,t,typ) acc -> + match typ with + | Some typ -> + CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else - Constrexpr.CProdN - (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + | None -> + CAst.make @@ Constrexpr.CProdN + ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1304,8 +1367,9 @@ let do_build_inductive *) let rel_arities = Array.mapi rel_arity funsargs in Util.Array.fold_left2 (fun env rel_name rel_ar -> - Environ.push_named (LocalAssum (rel_name, - fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) env) env relnames rel_arities + let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in + let rex = EConstr.Unsafe.to_constr rex in + Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = @@ -1346,19 +1410,19 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = (snd (List.chop nrel_params funargs)) in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + (fun (n,t,typ) acc -> + match typ with + | Some typ -> + CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else - Constrexpr.CProdN - (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + | None -> + CAst.make @@ Constrexpr.CProdN + ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1382,20 +1446,21 @@ let do_build_inductive in let rel_params = List.map - (fun (n,t,is_defined) -> - if is_defined - then - Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) - else - Constrexpr.LocalRawAssum - ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) + (fun (n,t,typ) -> + match typ with + | Some typ -> + Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) + | None -> + Constrexpr.CLocalAssum + ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params in let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((Loc.ghost,id), + false,((CAst.make id), with_full_print (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t)) ) @@ -1403,7 +1468,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((Loc.ghost,relnames.(i)), None), + (((CAst.make @@ relnames.(i)), None), rel_params, Some rel_arities.(i), ext_rel_constructors),[] @@ -1432,7 +1497,9 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1443,7 +1510,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1458,7 +1525,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in |