diff options
-rw-r--r-- | parsing/astterm.ml | 726 |
1 files changed, 726 insertions, 0 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml new file mode 100644 index 000000000..6746de065 --- /dev/null +++ b/parsing/astterm.ml @@ -0,0 +1,726 @@ + +(* $Id$ *) + +open Std;; +open Pp;; +open Names;; +open Ast;; +open Vectops;; +open Generic;; +open Term;; +open Environ;; +open Termenv;; +open Impuniv;; +open Himsg;; +open Multcase_astterm;; +open Evd;; +open More_util;; +open Rawterm;; + +(** Multcases ... **) + +let prpattern k p = Printer.gencompr CCI (Termast.ast_of_pat p) + +(* when an head ident is not a constructor in pattern *) +let mssg_hd_is_not_constructor s = + [< 'sTR ("The symbol "^s^" should be a constructor") >] +;; + +(* checking linearity of a list of ids in patterns *) +let non_linearl_mssg id = + [<'sTR "The variable " ; 'sTR(string_of_id id); + 'sTR " is bound several times in pattern" >] + +let rec has_duplicate = function + [] -> None + | x::l -> if List.mem x l then (Some x) else has_duplicate l + +let check_linearity loc ids = + match has_duplicate ids with + | Some id -> user_err_loc (loc,"dbize_eqn",non_linearl_mssg id) + | None -> () + +let mal_formed_mssg () = + [<'sTR "malformed macro of multiple case" >];; + +(* determines if some pattern variable starts with uppercase *) +let warning_uppercase loc uplid = (* Comment afficher loc ?? *) + let vars = + prlist_with_sep pr_spc (fun v -> [< 'sTR (string_of_id v) >]) uplid in + let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in + wARN [<'sTR ("Warning: the variable"^s1); vars; + 'sTR (" start"^s2^" with upper case in pattern"); 'cUT >] + +let is_uppercase_var v = + match (string_of_id v).[0] with + 'A'..'Z' -> true + | _ -> false + +let check_uppercase loc ids = + let uplid = filter is_uppercase_var ids in + if uplid <> [] then warning_uppercase loc uplid + +(* check that the number of pattern matches the number of matched args *) +let mssg_number_of_patterns n pl = + [< 'sTR"Expecting ";'iNT n ; 'sTR" pattern(s) but found "; + 'iNT (List.length pl); 'sTR" in " >] + +let check_number_of_pattern loc n l = + if n<>(List.length l) then + user_err_loc (loc,"check_number_of_pattern",mssg_number_of_patterns n l) + +(* absolutize_eqn replaces pattern variables that are global. This + * means that we are going to remove the pattern abstractions that + * correspond to constructors. + * Warning: Names that are global but do not correspond to + * constructors are considered non-known_global. E.g. if nat appears + * in a pattern is considered as a variable name. known_global should + * be refined in order to consider known_global names only those that + * correspond to constructors of inductive types. + *) +(* +let is_constructor = function + DOPN(MutConstruct((sp,tyi),i),cl)-> true | _ ->false + +let is_known_constructor k env id = + let srch = + match k with + CCI -> Machops.search_reference + | FW -> Machops.search_freference + | _ -> anomaly "known_global" in + try is_constructor (srch env id) + with (Not_found | UserError _) -> + (try is_constructor (Environ.search_synconst k id) + with Not_found -> false) +;; + +let rec abs_eqn k env avoid = function + (v::ids, Slam(_,ona,t)) -> + let id = id_of_string (Ast.id_of_ast v) in + if is_known_constructor k env id + then abs_eqn k env avoid (ids, subst1 (VAR id) t) + else + let id' = if is_underscore id then id else next_ident_away id avoid in + let (nids,nt) = abs_eqn k env (id'::avoid) (ids,t) in + (id'::nids, DLAM(na,nt)) + | ([],t) -> ([],t) + | _ -> assert false +;; + +let rec absolutize_eqn absrec k env = function + DOP1(XTRA("LAMEQN",ids),lam_eqn) -> + let gids = ids_of_sign (get_globals env) in + let (nids,neqn) = abs_eqn k env gids (ids, lam_eqn) in + let uplid = filter is_uppercase_var nids in + let _ = if uplid <> [] then warning_uppercase uplid in + DOP1(XTRA("LAMEQN",nids), absrec neqn) + | _ -> anomalylabstrm "absolutize_eqn" (mal_formed_mssg()) +;; +*) +(****************************************************************) +(* Arguments normally implicit in the "Implicit Arguments mode" *) +(* but explicitely given *) +(* +let dest_explicit_arg = function + (DOP1(XTRA ("!", [Num(_,j)]), t)) -> (j,t) + | _ -> raise Not_found + +let is_explicit_arg = function + (DOP1(XTRA ("!", [Num(_,j)]), t)) -> true + | _ -> false + +let explicitize_appl l args = + let rec aux n l args acc = + match (l,args) with + (i::l',a::args') -> + if i=n + then try let j,a' = dest_explicit_arg a in + if j > i + then aux (n+1) l' args (mkExistential::acc) + else if j = i + then aux (n+1) l' args' (a'::acc) + else error "Bad explicitation number" + with Not_found -> aux (n+1) l' args (mkExistential::acc) + else if is_explicit_arg a then error "Bad explicitation number" + else aux (n+1) l args' (a::acc) + | ([],_) -> (List.rev acc)@args + | (_,[]) -> (List.rev acc) +in aux 1 l args [] +;; + +let absolutize k sigma env constr = + let rec absrec env constr = match constr with + VAR id -> fst (absolutize_var_with_impl k sigma env id) + | Rel _ as t -> t + | DOP1(XTRA ("!", [Num _]), _) -> error "Bad explicitation number" + | DOPN(AppL,cl) -> (* Detect implicit args occurrences *) + let cl1 = Array.to_list cl in + let f = List.hd cl1 in + let args = List.tl cl1 in + begin match f with + VAR id -> + let (c, impargs) = absolutize_var_with_impl k sigma env id in + let newargs = explicitize_appl impargs args in + mkAppList c (List.map (absrec env) newargs) + | DOPN((Const _ | MutInd _ | MutConstruct _) as op, _) -> + let id = id_of_global op in + let (c, impargs) = search_ref_with_impl k env id in + let newargs = explicitize_appl impargs args in + mkAppList c (List.map (absrec env) newargs) + | (DOP1(XTRA ("!",[]), t)) -> + mkAppList (absrec env t) (List.map (absrec env) args) + | _ -> mkAppL (Array.map (absrec env) cl) + end + + (* Pattern branches have a special absolutization *) + | DOP1(XTRA("LAMEQN",_),_) as eqn -> absolutize_eqn (absrec env) k env eqn + + | DOP0 _ as t -> t + | DOP1(oper,c) -> DOP1(oper,absrec env c) + | DOP2(oper,c1,c2) -> DOP2(oper,absrec env c1,absrec env c2) + | DOPN(oper,cl) -> DOPN(oper,Array.map (absrec env) cl) + | DOPL(oper,cl) -> DOPL(oper,List.map (absrec env) cl) + | DLAM(na,c) -> DLAM(na,absrec (add_rel (na,()) env) c) + | DLAMV(na,cl) -> DLAMV(na,Array.map (absrec (add_rel (na,()) env)) cl) + + in absrec env constr +;; + +(* Fonctions exportées *) +let absolutize_cci sigma env constr = absolutize CCI sigma env constr +let absolutize_fw sigma env constr = absolutize FW sigma env constr +*) + +let dbize_sp = function + Path(loc,sl,s) -> + (try section_path sl s + with Invalid_argument _ | Failure _ -> + anomaly_loc(loc,"Astterm.dbize_sp", + [< 'sTR"malformed section-path" >])) + | ast -> anomaly_loc(Ast.loc ast,"Astterm.dbize_sp", + [< 'sTR"not a section-path" >]);; +(* +let dbize_op loc opn pl cl = + match (opn,pl,cl) with + ("META",[Num(_,n)], []) -> DOP0(Meta n) + | ("XTRA",(Str(_,s))::tlpl,_) when (multcase_kw s) -> + DOPN(XTRA(s,tlpl),Array.of_list cl) + | ("XTRA",(Str(_,s))::tlpl,[]) -> DOP0(XTRA(s,tlpl)) + | ("XTRA",(Str(_,s))::tlpl,[c]) -> DOP1(XTRA(s,tlpl),c) + | ("XTRA",(Str(_,s))::tlpl,[c1;c2]) -> DOP2(XTRA(s,tlpl),c1,c2) + | ("XTRA",(Str(_,s))::tlpl,_) -> DOPN(XTRA(s,tlpl), Array.of_list cl) + + | ("PROP", [Id(_,s)], []) -> + (try RSort(Prop (contents_of_str s)) + with Invalid_argument s -> anomaly_loc (loc,"Astterm.dbize_op", + [< 'sTR s >])) + | ("TYPE", [], []) -> RSort(Type(dummy_univ)) + + | ("IMPLICIT", [], []) -> DOP0(Implicit) + | ("CAST", [], [c1;c2]) -> DOP2(Cast,c1,c2) + + | ("CONST", [sp], _) -> DOPN(Const (dbize_sp sp),Array.of_list cl) + | ("ABST", [sp], _) -> + (try global_abst (dbize_sp sp) (Array.of_list cl) + with + Failure _ | Invalid_argument _ -> + anomaly_loc(loc,"Astterm.dbize_op", + [< 'sTR"malformed abstraction" >]) + | Not_found -> user_err_loc(loc,"Astterm.dbize_op", + [< 'sTR"Unbound abstraction" >])) + | ("MUTIND", [sp;Num(_,tyi)], _) -> + DOPN(MutInd (dbize_sp sp, tyi),Array.of_list cl) + + | ("MUTCASE", [], p::c::l) -> mkMutCase None p c l + + | ("MUTCONSTRUCT", [sp;Num(_,tyi);Num(_,n)], _) -> + DOPN(MutConstruct ((dbize_sp sp, tyi),n),Array.of_list cl) + + | ("SQUASH",[],[_]) -> user_err_loc + (loc,"Astterm.dbize_op", + [< 'sTR "Unrecognizable braces expression." >]) + + | (op,_,_) -> anomaly_loc + (loc,"Astterm.dbize_op", + [< 'sTR "Unrecognizable constr operator: "; 'sTR op >]) +;; + +let split_params = + let rec sprec acc = function + (Id _ as p)::l -> sprec (p::acc) l + | (Str _ as p)::l -> sprec (p::acc) l + | (Num _ as p)::l -> sprec (p::acc) l + | (Path _ as p)::l -> sprec (p::acc) l + | l -> (List.rev acc,l) + in sprec [] +;; +*) + +let is_underscore id = (id = "_") + +let name_of_nvar s = + if is_underscore s then Anonymous else Name (id_of_string s) + +let ident_of_nvar loc s = + if is_underscore s then + user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >]) + else (id_of_string s) + +let ids_of_ctxt = Termast.ids_of_ctxt + +let maybe_constructor env s = + try match Machops.search_reference env (id_of_string s) with + DOPN(MutConstruct (spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl) + | _ -> None + with Not_found -> None + +let dbize_ctxt = + List.map + (function + | Nvar (loc,s) -> ident_of_nvar loc s + | _ -> anomaly "Bad ast for local ctxt of a global reference") + +let dbize_global loc = function + | ("CONST", sp::ctxt) -> RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt)) + | ("EVAR", sp::ctxt) -> RRef (loc,REVar (dbize_sp sp,dbize_ctxt ctxt)) + | ("MUTIND", sp::Num(_,tyi)::ctxt) -> RRef (loc,RInd ((dbize_sp sp, tyi),dbize_ctxt ctxt)) + | ("MUTCONSTRUCT", sp::Num(_,ti)::Num(_,n)::ctxt) -> + RRef (loc,RConstruct (((dbize_sp sp,ti),n),dbize_ctxt ctxt)) + | ("SYNCONST", [sp]) -> search_synconst_path CCI (dbize_sp sp) +(* | ("ABST", [sp]) -> RRef (loc,Abst (dbize_sp sp)) *) + | _ -> anomaly_loc (loc,"dbize_global", + [< 'sTR "Bad ast for this global a reference">]) + +let ref_from_constr = function + | DOPN (Const sp,ctxt) -> + if is_existential_id (basename sp) + then REVar (sp,ids_of_ctxt ctxt) + else RConst (sp,ids_of_ctxt ctxt) + | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j),ids_of_ctxt ctxt) + | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i),ids_of_ctxt ctxt) + | VAR id -> RVar id (* utilisé dans trad pour coe_value (tmp) *) + | _ -> anomaly "Not a reference" + +let dbize_ref k sigma env loc s = + let id = ident_of_nvar loc s in + if (is_existential_id id) then + match k with + CCI -> + RRef (loc,ref_from_constr ( + Machops.lookup_exist sigma env (evar_of_id k id))),[] + | FW -> error "existentials in fterms not implemented" + | OBJ -> anomaly "absolutize_var" + else + try match lookup_id id env with + RELNAME(n,_) -> RRel (loc,n),[] + | _ -> RRef(loc,RVar id), (try Vartab.implicits_of_var k id with _ -> []) + with Not_found -> + try let c,il = match k with + CCI -> Machops.search_reference1 env id + | FW -> Machops.search_freference1 env id + | OBJ -> anomaly "search_ref_cci_fw" in + RRef (loc,ref_from_constr c), il + with UserError _ -> + try (search_synconst k id,[]) + with Not_found -> error_var_not_found "dbize_ref" loc s + + +let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)]) +let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) +let mkProdC (x,a,b) = ope("PROD",[a;slam(Some (string_of_id x),b)]) +let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) +let destruct_binder = function + Node(_,"BINDER",c::idl) -> + List.map (fun id -> (id_of_string (nvar_of_ast id),c)) idl + | _ -> anomaly "BINDER is expected" + +let rec dbize_pattern env = function + | Node(_,"PATTAS",[Nvar (loc,s); p]) -> + (match name_of_nvar s with + Anonymous -> dbize_pattern env p + | Name id -> + let (ids,p') = dbize_pattern env p in (id::ids,PatAs (loc,id,p'))) + | Node(_,"PATTCONSTRUCT", Nvar(loc,s)::((_::_) as pl)) -> + (match maybe_constructor env s with + | Some c -> + let (idsl,pl') = List.split (List.map (dbize_pattern env) pl) in + (List.flatten idsl,PatCstr (loc,c,pl')) + | None -> + user_err_loc (loc,"dbize_pattern",mssg_hd_is_not_constructor s)) + | Nvar(loc,s) -> + (match name_of_nvar s with + Anonymous -> ([], PatVar (loc,Anonymous)) + | Name id as name -> ([id], PatVar (loc,name))) + | _ -> anomaly "dbize: badly-formed ast for Cases pattern" + +let rec dbize_fix = function + | [] -> ([],[],[],[]) + | Node(_,"NUMFDECL", [Nvar(_,fi); Num(_,ni); astA; astT])::rest -> + let (lf,ln,lA,lt) = dbize_fix rest in + ((id_of_string fi)::lf, (ni-1)::ln, astA::lA, astT::lt) + | Node(_,"FDECL", [Nvar(_,fi); Node(_,"BINDERS",bl); astA; astT])::rest -> + let binders = List.flatten (List.map destruct_binder bl) in + let ni = List.length binders - 1 in + let (lf,ln,lA,lt) = dbize_fix rest in + ((id_of_string fi)::lf, ni::ln, (mkProdCit binders astA)::lA, + (mkLambdaCit binders astT)::lt) + | _ -> anomaly "FDECL or NUMFDECL is expected" + +let rec dbize_cofix = function + | [] -> ([],[],[]) + | Node(_,"CFDECL", [Nvar(_,fi); astA; astT])::rest -> + let (lf,lA,lt) = dbize_cofix rest in + ((id_of_string fi)::lf, astA::lA, astT::lt) + | _ -> anomaly "CFDECL is expected" + +let dbize k sigma = + let rec dbrec env = function + Nvar(loc,s) -> fst (dbize_ref k sigma env loc s) + +(* + | Slam(_,ona,Node(_,"V$",l)) -> + let na = + (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous) + in DLAMV(na,Array.of_list (List.map (dbrec (add_rel (na,()) env)) l)) + + | Slam(_,ona,t) -> + let na = + (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous) + in DLAM(na, dbrec (add_rel (na,()) env) t) +*) + | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) -> + let (lf,ln,lA,lt) = dbize_fix ldecl in + let n = + try (index (ident_of_nvar locid iddef) lf) -1 + with Failure _ -> + error_fixname_unbound "dbize (FIX)" false locid iddef in + let ext_env = + List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in + let defl = Array.of_list (List.map (dbrec ext_env) lt) in + let arityl = Array.of_list (List.map (dbrec env) lA) in + RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl) + + | Node(loc,"COFIX", (Nvar(locid,iddef))::ldecl) -> + let (lf,lA,lt) = dbize_cofix ldecl in + let n = + try (index (ident_of_nvar locid iddef) lf) -1 + with Failure _ -> + error_fixname_unbound "dbize (COFIX)" true locid iddef in + let ext_env = + List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in + let defl = Array.of_list (List.map (dbrec ext_env) lt) in + let arityl = Array.of_list (List.map (dbrec env) lA) in + RRec (loc,RCofix n, Array.of_list lf, arityl, defl) + + | Node(loc,("PROD"|"LAMBDA" as k), [c1;Slam(_,ona,c2)]) -> + let na = match ona with + Some s -> Name (id_of_string s) + | _ -> Anonymous in + let kind = if k="PROD" then BProd else BLambda in + RBinder(loc, kind, na, dbrec env c1, dbrec (add_rel (na,()) env) c2) + | Node(_,"PRODLIST", [c1;(Slam _ as c2)]) -> iterated_binder BProd c1 env c2 + | Node(_,"LAMBDALIST", [c1;(Slam _ as c2)]) -> iterated_binder BLambda c1 env c2 + + | Node(loc,"APPLISTEXPL", f::args) -> + RApp (loc,dbrec env f,List.map (dbrec env) args) + | Node(loc,"APPLIST", Nvar(locs,s)::args) -> + let (c, impargs) = dbize_ref k sigma env locs s in + RApp (loc, c, dbize_args env impargs args) + | Node(loc,"APPLIST", f::args) -> + RApp (loc,dbrec env f,List.map (dbrec env) args) + + | Node(loc,"MULTCASE", p:: Node(_,"TOMATCH",tms):: eqns) -> + let po = match p with Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in + RCases (loc,PrintCases,po, + List.map (dbrec env) tms, + List.map (dbize_eqn (List.length tms) env) eqns) + + | Node(loc,"CASE",Str(_,isrectag)::p::c::cl) -> + let po = match p with Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in + let isrec = match isrectag with + | "REC" -> true | "NOREC" -> false + | _ -> anomaly "dbize: wrong REC tag in CASE" in + ROldCase (loc,isrec,po,dbrec env c,Array.of_list (List.map (dbrec env) cl)) + + | Node(loc,"ISEVAR",[]) -> RHole (Some loc) + | Node(loc,"META",[Num(_,n)]) -> RRef (loc,RMeta n) + + | Node(loc,"PROP", []) -> RSort(loc,RProp Null) + | Node(loc,"SET", []) -> RSort(loc,RProp Pos) + | Node(loc,"TYPE", []) -> RSort(loc,RType) + + (* This case mainly parses things build from in a quotation *) + | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) -> + dbize_global loc (key,l) + + | Node(loc,opn,tl) -> anomaly ("dbize found operator "^opn^" with "^(string_of_int (List.length tl))^" arguments") + + | _ -> anomaly "dbize: unexpected ast" + + and dbize_eqn n env = function + | Node(loc,"EQN",rhs::lhs) -> + let (idsl,pl) = List.split (List.map (dbize_pattern env) lhs) in + let ids = List.flatten idsl in + check_linearity loc ids; + check_uppercase loc ids; + check_number_of_pattern loc n pl; + let env' = + List.fold_left (fun env id -> add_rel (Name id,()) env) env ids in + (ids,pl,dbrec env' rhs) + | _ -> anomaly "dbize: badly-formed ast for Cases equation" + + and iterated_binder oper ty env = function + Slam(loc,ona,body) -> + let na = + (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous) + in RBinder(loc, oper, na, + dbrec (add_rel (Anonymous,()) env) ty, (* To avoid capture *) + (iterated_binder oper ty (add_rel (na,()) env) body)) + | body -> dbrec env body + + and dbize_args env l args = + let rec aux n l args = match (l,args) with + | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') -> + if i=n & j>=i then + if j=i + then (dbrec env a)::(aux (n+1) l' args') + else (RHole None)::(aux (n+1) l' args) + else error "Bad explicitation number" + | (i::l',a::args') -> + if i=n + then (RHole None)::(aux (n+1) l' args) + else (dbrec env a)::(aux (n+1) l' args') + | ([],args) -> List.map (dbrec env) args + | (_,[]) -> [] + in aux 1 l args + + in dbrec +;; + +(* +let dbize_kind ... = + let c = + try dbize k sigma env com + with e -> + wrap_error + (Ast.loc com, "dbize_kind", + [< 'sTR"During conversion from explicit-names to" ; 'sPC ; + 'sTR"debruijn-indices" >], e, + [< 'sTR"Perhaps the input is malformed" >]) in + + let c = + try absolutize k sigma env c + with e -> + wrap_error + (Ast.loc com, "Astterm.dbize_kind", + [< 'sTR"During the relocation of global references," >], e, + [< 'sTR"Perhaps the input is malformed" >]) + in c +;; +*) + +let dbize_cci sigma env com = dbize CCI sigma env com +let dbize_fw sigma env com = dbize FW sigma env com + +(* constr_of_com takes an environment of typing assumptions, + * and translates a command to a constr. + +let raw_constr_of_com sigma env com = + let c = dbize_cci sigma (unitize_env env) com in + try Sosub.soexecute c + with Failure _|UserError _ -> error_sosub_execute CCI com;; + +let raw_fconstr_of_com sigma env com = + let c = dbize_fw sigma (unitize_env env) com in + try Sosub.soexecute c + with Failure _|UserError _ -> error_sosub_execute FW com;; + +let raw_constr_of_compattern sigma env com = + let c = dbize_cci sigma (unitize_env env) com in + try Sosub.try_soexecute c + with Failure _|UserError _ -> error_sosub_execute CCI com;; + *) + +let raw_constr_of_com sigma env com = dbize_cci sigma (unitize_env env) com +let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env env) com +let raw_constr_of_compattern sigma env com = + dbize_cci sigma (unitize_env env) com + + +(* Globalization of AST quotations (mainly used in command quotations + to get statically bound idents in grammar or pretty-printing rules) *) + +let ast_adjust_consts sigma = (* locations are kept *) + let rec dbrec env = function + Nvar(loc,s) as ast -> + (let id = id_of_string s in + if (Ast.isMeta s) or (is_existential_id id) then ast + else if List.mem id (ids_of_env env) then ast + else + try match Machops.search_reference env id with + | DOPN (Const sp,_) -> + if is_existential_id (basename sp) + then Node(loc,"EVAR",[path_section loc sp]) + else Node(loc,"CONST",[path_section loc sp]) + | DOPN (MutConstruct ((sp,i),j),_) -> + Node (loc,"MUTCONSTRUCT",[path_section loc sp;num i;num j]) + | DOPN (MutInd (sp,i),_) -> + Node (loc,"MUTIND",[path_section loc sp;num i]) + | _ -> anomaly "Not a reference" + with UserError _ | Not_found -> + try let _ = search_synconst CCI id in Node(loc,"SYNCONST",[Nvar(loc,s)]) + with Not_found -> warning ("Could not globalize "^s); ast) + + | Slam(loc,None,t) -> Slam(loc,None,dbrec (add_rel (Anonymous,()) env) t) + + | Slam(loc,Some na,t) -> + let env' = add_rel (Name (id_of_string na),()) env in + Slam(loc,Some na,dbrec env' t) + | Node(loc,opn,tl) -> Node(loc,opn,List.map (dbrec env) tl) + | x -> x + in dbrec +;; + + +let globalize_command ast = + let (sigma,sign) = Termenv.initial_sigma_sign() in + ast_adjust_consts sigma (gLOB sign) ast +;; + + +(* Avoid globalizing in non command ast for tactics *) +let rec glob_ast sigma env = function + | Node(loc,"COMMAND",[c]) -> + Node(loc,"COMMAND",[ast_adjust_consts sigma env c]) + | Node(loc,"COMMANDLIST",l) -> + Node(loc,"COMMANDLIST", List.map (ast_adjust_consts sigma env) l) + | Slam(loc,None,t) -> + Slam(loc,None,glob_ast sigma (add_rel (Anonymous,()) env) t) + | Slam(loc,Some na,t) -> + let env' = add_rel (Name (id_of_string na),()) env in + Slam(loc,Some na, glob_ast sigma env' t) + | Node(loc,opn,tl) -> Node(loc,opn,List.map (glob_ast sigma env) tl) + | x -> x +;; + +let globalize_ast ast = + let (sigma,sign) = Termenv.initial_sigma_sign() in + glob_ast sigma (gLOB sign) ast +;; + +(* Installation of the AST quotations. "command" is used by default. *) +open Pcoq;; +define_quotation true "command" (map_entry globalize_command Command.command);; +define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic);; +define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac);; + + +(*********************************************************************) +(* Functions before in ex-trad *) + +(* Endless list of alternative ways to call Trad *) + +(* With dB *) + +let constr_of_com_env1 is_ass sigma hyps com = + let c = Astterm.raw_constr_of_com sigma hyps com in + try ise_resolve1 is_ass sigma hyps c + with e -> Stdpp.raise_with_loc (Ast.loc com) e + + +let constr_of_com_env sigma hyps com = + constr_of_com_env1 false sigma hyps com + +let fconstr_of_com_env1 is_ass sigma hyps com = + let c = Astterm.raw_fconstr_of_com sigma hyps com in + try ise_resolve1 is_ass sigma hyps c + with e -> Stdpp.raise_with_loc (Ast.loc com) e + + +let fconstr_of_com_env sigma hyps com = + fconstr_of_com_env1 false sigma hyps com + + +(* Without dB *) +let type_of_com sign com = + let env = gLOB sign in + let c = Astterm.raw_constr_of_com mt_evd env com in + try ise_resolve_type true mt_evd [] env c + with e -> Stdpp.raise_with_loc (Ast.loc com) e + + +let constr_of_com1 is_ass sigma sign com = + constr_of_com_env1 is_ass sigma (gLOB sign) com + +let constr_of_com sigma sign com = + constr_of_com1 false sigma sign com +let constr_of_com_sort sigma sign com = + constr_of_com1 true sigma sign com + +let fconstr_of_com1 is_ass sigma sign com = + fconstr_of_com_env1 is_ass sigma (gLOB sign) com + +let fconstr_of_com sigma sign com = + fconstr_of_com1 false sigma sign com +let fconstr_of_com_sort sigma sign com = + fconstr_of_com1 true sigma sign com + +(* Note: typ is retyped *) +let constr_of_com_casted sigma sign com typ = + let env = gLOB sign in + let c = Astterm.raw_constr_of_com sigma env com in + let isevars = ref sigma in + try + let j = unsafe_fmachine + (mk_tycon (nf_ise1 sigma typ)) false isevars [] env c in + (j_apply (process_evars true !isevars) j)._VAL + with e -> Stdpp.raise_with_loc (Ast.loc com) e + + + +(* Typing with Trad, and re-checking with Mach *) +let fconstruct_type sigma sign com = + let c = constr_of_com1 true sigma sign com + in Mach.fexecute_type sigma sign c + +let fconstruct sigma sign com = + let c = constr_of_com1 false sigma sign com + in Mach.fexecute sigma sign c + +let infconstruct_type sigma (sign,fsign) cmd = + let c = constr_of_com1 true sigma sign cmd + in Mach.infexecute_type sigma (sign,fsign) c + +let infconstruct sigma (sign,fsign) cmd = + let c = constr_of_com1 false sigma sign cmd + in Mach.infexecute sigma (sign,fsign) c + +(* Type-checks a term with the current universe constraints, the resulting + constraints are dropped. *) +let univ_sp = make_path ["univ"] (id_of_string "dummy") OBJ +let fconstruct_with_univ sigma sign com = + let c = constr_of_com sigma sign com in + let(_,j) = with_universes (Mach.fexecute sigma sign) + (univ_sp, Constraintab.current_constraints(), c) + in j + + +(* Keeping universe constraints *) +let fconstruct_type_with_univ_sp sigma sign sp c = + with_universes + (Mach.fexecute_type sigma sign) (sp,initial_universes,c) + + +let fconstruct_with_univ_sp sigma sign sp c = + with_universes + (Mach.fexecute sigma sign) (sp,initial_universes,c) + + +let infconstruct_type_with_univ_sp sigma (sign,fsign) sp c = + with_universes + (Mach.infexecute_type sigma (sign,fsign)) (sp,initial_universes,c) + + +let infconstruct_with_univ_sp sigma (sign,fsign) sp c = + with_universes + (Mach.infexecute sigma (sign,fsign)) (sp,initial_universes,c) |