exception Macro of
GrafiteAst.loc *
(Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
+exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
do_heavy_checks: bool ;
}
+let concat_nuris uris nuris =
+ match uris,nuris with
+ | `New uris, `New nuris -> `New (nuris@uris)
+ | _ -> assert false
+;;
(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
* names as long as they are available, then it fallbacks to name generation
* using FreshNamesGenerator module *)
status,`New []
;;
-let basic_eval_ncoercion (name,t,s,d,p,a) status =
- NCicCoercion.index_coercion status t s d a p
-;;
-
-let inject_ncoercion =
- let basic_eval_ncoercion x ~refresh_uri_in_universe ~refresh_uri_in_term =
- basic_eval_ncoercion x
- in
- NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
-;;
-
-let eval_ncoercion status name t ty (id,src) tgt =
-
- let metasenv,subst,status,ty =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
- assert (metasenv=[]);
- let ty = NCicUntrusted.apply_subst subst [] ty in
- let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
- assert (metasenv=[]);
- let t = NCicUntrusted.apply_subst subst [] t in
-
- let src, cpos =
- let rec aux cpos ctx = function
- | NCic.Prod (name,ty,bo) ->
- if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
- else
- let metasenv,subst,status,src =
- GrafiteDisambiguate.disambiguate_nterm
- None status ctx [] [] ("",0,src) in
- let src = NCicUntrusted.apply_subst subst [] src in
- (* HMM: ma tanto se ignori l'informazione, a che serve?? *)
- let _ = NCicUnification.unify status metasenv subst ctx ty src in
- src, cpos
- | _ -> assert false
- in
- aux 0 [] ty
- in
- let tgt, arity =
- let metasenv,subst,status,tgt =
- GrafiteDisambiguate.disambiguate_nterm
- None status [] [] [] ("",0,tgt) in
- let tgt = NCicUntrusted.apply_subst subst [] tgt in
- (* CHECK *)
- let rec count_prod = function
- | NCic.Prod (_,_,x) -> 1 + count_prod x
- | _ -> 0
- in
- tgt, count_prod tgt
- in
-
- let status = basic_eval_ncoercion (name,t,src,tgt,cpos,arity) status in
- let dump = inject_ncoercion (name,t,src,tgt,cpos,arity)::status#dump in
- let status = status#set_dump dump in
- status,`New []
-;;
-
-let basic_eval_add_constraint (s,u1,u2) status =
- NCicLibrary.add_constraint status s u1 u2
+let basic_eval_add_constraint (u1,u2) status =
+ NCicLibrary.add_constraint status u1 u2
;;
let inject_constraint =
- let basic_eval_add_constraint (s,u1,u2)
+ let basic_eval_add_constraint (u1,u2)
~refresh_uri_in_universe
~refresh_uri_in_term
=
let u1 = refresh_uri_in_universe u1 in
let u2 = refresh_uri_in_universe u2 in
- basic_eval_add_constraint (s,u1,u2)
+ basic_eval_add_constraint (u1,u2)
in
NRstatus.Serializer.register "constraints" basic_eval_add_constraint
;;
-let eval_add_constraint status s u1 u2 =
- let status = basic_eval_add_constraint (s,u1,u2) status in
- let dump = inject_constraint (s,u1,u2)::status#dump in
+let eval_add_constraint status u1 u2 =
+ let status = basic_eval_add_constraint (u1,u2) status in
+ let dump = inject_constraint (u1,u2)::status#dump in
let status = status#set_dump dump in
status,`Old []
;;
| GrafiteAst.NChange (_loc, pat, ww) ->
NTactics.change_tac
~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww)
+ | GrafiteAst.NConstructor (_loc,num,args) ->
+ NTactics.constructor_tac
+ ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
+ | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
NTactics.elim_tac
NTactics.generalize_tac ~where:(text,prefix_len,where)
| GrafiteAst.NId _ -> (fun x -> x)
| GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+ | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t)
| GrafiteAst.NLetIn (_loc,where,what,name) ->
NTactics.letin_tac ~where:(text,prefix_len,where)
~what:(text,prefix_len,what) name
match cmd with
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
- eval_ncoercion status name t ty source target
+ NCicCoercDeclaration.eval_ncoercion status name t ty source target
| GrafiteAst.NQed loc ->
if status#ng_mode <> `ProofMode then
raise (GrafiteTypes.Command_error "Not in proof mode")
| _ -> obj_kind
in
let obj = uri,height,[],[],obj_kind in
- let status = NCicLibrary.add_obj status obj in
- let objs = NCicElim.mk_elims obj in
- let timestamp,uris_rev =
- List.fold_left
- (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
- let status = NCicLibrary.add_obj status obj in
- status,uri::uris_rev
- ) (status,[]) objs in
- let uris = uri::List.rev uris_rev in
- status#set_ng_mode `CommandMode,`New uris
+ let old_status = status in
+ let status = NCicLibrary.add_obj status obj in
+ HLog.message ("New object: " ^ NUri.string_of_uri uri);
+ (try
+ (*prerr_endline (NCicPp.ppobj obj);*)
+ let boxml = NCicElim.mk_elims obj in
+ let boxml = boxml @ NCicElim.mk_projections obj in
+(*
+ let objs = [] in
+ let timestamp,uris_rev =
+ List.fold_left
+ (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
+ let status = NCicLibrary.add_obj status obj in
+ status,uri::uris_rev
+ ) (status,[]) objs in
+ let uris = uri::List.rev uris_rev in
+*)
+ let status = status#set_ng_mode `CommandMode in
+ let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
+ let status,uris =
+ List.fold_left
+ (fun (status,uris) boxml ->
+ try
+ let status,nuris =
+ eval_ncommand opts status
+ ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+ in
+ status, concat_nuris uris nuris
+ with
+ | MultiPassDisambiguator.DisambiguationError _
+ | NCicTypeChecker.TypeCheckerFailure _ ->
+ HLog.warn "error in generating projection/eliminator";
+ status,uris
+ ) (status,`New [] (* uris *)) boxml in
+ let coercions =
+ match obj with
+ _,_,_,_,NCic.Inductive
+ (true,leftno,[_,_,_,[_,_,_]],(_,`Record fields))
+ ->
+ HExtlib.filter_map
+ (fun (name,is_coercion,arity) ->
+ if is_coercion then Some(name,leftno,arity) else None) fields
+ | _ -> [] in
+ let status,uris =
+ List.fold_left
+ (fun (status,uris) (name,cpos,arity) ->
+ try
+ let metasenv,subst,status,t =
+ GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+ ("",0,CicNotationPt.Ident (name,None)) in
+ assert (metasenv = [] && subst = []);
+ let status, nuris =
+ NCicCoercDeclaration.
+ basic_eval_and_record_ncoercion_from_t_cpos_arity
+ status (name,t,cpos,arity)
+ in
+ let uris = concat_nuris nuris uris in
+ status, uris
+ with MultiPassDisambiguator.DisambiguationError _->
+ HLog.warn ("error in generating coercion: "^name);
+ status, uris)
+ (status,uris) coercions
+ in
+ status,uris
+ with
+ exn ->
+ NCicLibrary.time_travel old_status;
+ raise exn)
+ | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
+ if status#ng_mode <> `CommandMode then
+ raise (GrafiteTypes.Command_error "Not in command mode")
+ else
+ let tgt_uri_ext, old_ok =
+ match NCicEnvironment.get_checked_obj src_uri with
+ | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok
+ | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok
+ | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok
+ | _ -> assert false
+ in
+ let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in
+ let map = (src_uri, tgt_uri) :: map in
+ let ok =
+ let rec subst () = function
+ | NCic.Meta _ -> assert false
+ | NCic.Const (NReference.Ref (u,spec)) as t ->
+ (try NCic.Const
+ (NReference.reference_of_spec (List.assoc u map)spec)
+ with Not_found -> t)
+ | t -> NCicUtils.map (fun _ _ -> ()) () subst t
+ in
+ NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok
+ in
+ let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+ let status = status#set_obj (tgt_uri,0,[],[],ok) in
+ (*prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));*)
+ let status = status#set_stack ninitial_stack in
+ let status = subst_metasenv_and_fix_names status in
+ let status = status#set_ng_mode `ProofMode in
+ eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| GrafiteAst.NObj (loc,obj) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
[] ->
eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> status,`New [])
- | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
- eval_add_constraint status strict [false,u1] [false,u2]
+ | GrafiteAst.NInverter (loc, name, indty) ->
+ if status#ng_mode <> `CommandMode then
+ raise (GrafiteTypes.Command_error "Not in command mode")
+ else
+ let status = status#set_ng_mode `ProofMode in
+ let metasenv,subst,status,indty =
+ GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
+ let _,leftno,tys,_,_ = match indty with
+ NCic.Const r -> NCicEnvironment.get_checked_indtys r
+ | _ -> assert false in
+ let it = match tys with
+ hd::tl -> hd
+ | _ -> assert false
+ in
+ let status,obj =
+ NInversion.mk_inverter name it leftno status status#baseuri in
+ let _,_,menv,_,_ = obj in
+ (match menv with
+ [] ->
+ eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ | _ -> assert false)
+ | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
+ eval_add_constraint status [`Type,u1] [`Type,u2]
;;
let rec eval_command = {ec_go = fun ~disambiguate_command opts status
eval_ncommand opts status (text,prefix_len,cmd)
| GrafiteAst.Macro (loc, macro) ->
raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro)))
+ | GrafiteAst.NMacro (loc, macro) ->
+ raise (NMacro (loc,macro))
} and eval_from_moo = {efm_go = fun status fname ->
let ast_of_cmd cmd =
projects / helm.git / blobdiff