diff options
Diffstat (limited to 'parsing/ast.ml')
| -rwxr-xr-x | parsing/ast.ml | 251 |
1 files changed, 33 insertions, 218 deletions
diff --git a/parsing/ast.ml b/parsing/ast.ml index 52a390af1..ae677979f 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -13,12 +13,11 @@ open Util open Names open Libnames open Coqast +open Topconstr open Genarg let isMeta s = String.length s <> 0 & s.[0]='$' -let dummy_loc = (0,0) - let loc = function | Node (loc,_,_) -> loc | Nvar (loc,_) -> loc @@ -31,17 +30,6 @@ let loc = function | Path (loc,_) -> loc | Dynamic (loc,_) -> loc -type entry_type = - | PureAstType - | IntAstType - | IdentAstType - | AstListType - | TacticAtomAstType - | ThmTokenAstType - | DynamicAstType - | ReferenceAstType - | GenAstType of Genarg.argument_type - (* patterns of ast *) type astpat = | Pquote of t @@ -107,19 +95,28 @@ let id_of_ast = function (* semantic actions of grammar rules *) type act = - | Act of pat + | Act of constr_expr | ActCase of act * (pat * act) list | ActCaseList of act * (pat * act) list (* values associated to variables *) +(* +type typed_ast = + | AstListNode of Coqast.t list + | PureAstNode of Coqast.t +*) type typed_ast = | AstListNode of Coqast.t list | PureAstNode of Coqast.t type ast_action_type = ETast | ETastl +type dynamic_grammar = + | ConstrNode of constr_expr + | CasesPatternNode of cases_pattern_expr + type grammar_action = - | SimpleAction of loc * typed_ast + | SimpleAction of loc * dynamic_grammar | CaseAction of loc * grammar_action * ast_action_type * (t list * grammar_action) list @@ -211,56 +208,25 @@ let rec coerce_to_var = function (loc ast,"Ast.coerce_to_var", (str"This expression should be a simple identifier")) -let coerce_to_id a = match coerce_to_var a with +let coerce_to_id_ast a = match coerce_to_var a with | Nvar (_,id) -> id | ast -> user_err_loc (loc ast,"Ast.coerce_to_id", str"This expression should be a simple identifier") -let coerce_qualid_to_id (loc,qid) = match repr_qualid qid with - | dir, id when dir = empty_dirpath -> id - | _ -> - user_err_loc (loc, "Ast.coerce_qualid_to_id", - str"This expression should be a simple identifier") +let coerce_to_id = function + | CRef (Ident (_,id)) -> id + | a -> user_err_loc + (constr_loc a,"Ast.coerce_to_id", + str"This expression should be a simple identifier") let coerce_reference_to_id = function - | RIdent (_,id) -> id - | RQualid (loc,_) -> + | Ident (_,id) -> id + | Qualid (loc,_) -> user_err_loc (loc, "Ast.coerce_reference_to_id", str"This expression should be a simple identifier") -(* This is to interpret the macro $ABSTRACT used in binders *) -(* $ABSTRACT should occur in this configuration : *) -(* ($ABSTRACT name (s1 a1 ($LIST l1)) ... (s2 an ($LIST ln)) b) *) -(* where li is id11::...::id1p1 and it produces the ast *) -(* (s1' a1 [id11]...[id1p1](... (sn' an [idn1]...[idnpn]b)...)) *) -(* where s1' is overwritten by name if s1 is $BINDER otherwise s1 *) - -let slam_ast (_,fin) id ast = - match id with - | Coqast.Nvar ((deb,_), s) -> - let name = if s = id_of_string "_" then None else Some s in - Coqast.Slam ((deb,fin), name, ast) - | Coqast.Nmeta ((deb,_), s) -> Coqast.Smetalam ((deb,fin), s, ast) - | _ -> invalid_arg "Ast.slam_ast" - -let abstract_binder_ast (_,fin as loc) name a b = - match a with - | Coqast.Node((deb,_),s,d::l) -> - let s' = if s="BINDER" then name else s in - Coqast.Node((deb,fin),s', [d; List.fold_right (slam_ast loc) l b]) - | _ -> invalid_arg "Bad usage of $ABSTRACT macro" - -let abstract_binders_ast loc name a b = - match a with - | Coqast.Node(_,"BINDERS",l) -> - List.fold_right (abstract_binder_ast loc name) l b - | _ -> invalid_arg "Bad usage of $ABSTRACT macro" - -let mkCastC(a,b) = ope("CAST",[a;b]) -let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)]) -let mkLetInC(x,a,b) = ope("LETIN",[a;slam(Some x,b)]) -let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)]) +let coerce_global_to_id = coerce_reference_to_id (* Pattern-matching on ast *) @@ -284,8 +250,8 @@ let env_assoc sigma k (loc,v) = let env_assoc_nvars sigma (dloc,v) = match env_assoc_value dloc v sigma with - | AstListNode al -> List.map coerce_to_id al - | PureAstNode ast -> [coerce_to_id ast] + | AstListNode al -> List.map coerce_to_id_ast al + | PureAstNode ast -> [coerce_to_id_ast ast] let build_lams dloc idl ast = List.fold_right (fun id lam -> Slam(dloc,Some id,lam)) idl ast @@ -488,7 +454,9 @@ let rec pat_of_ast env ast = | Node(_,op,args) -> let (pargs, env') = patl_of_astl env args in (Pnode(op,pargs), env') - | (Path _|Num _|Id _|Str _|Nvar _) -> (Pquote (set_loc dummy_loc ast), env) +(* Compatibility with new parsing mode *) + | Nvar(loc,id) when (string_of_id id).[0] = '$' -> make_astvar env loc (string_of_id id) Tany + | (Path _|Num _|Id _|Str _ |Nvar _) -> (Pquote (set_loc dummy_loc ast), env) | Dynamic(loc,_) -> invalid_arg_loc(loc,"pat_of_ast: dynamic") @@ -505,27 +473,15 @@ and patl_of_astl env astl = type entry_env = (string * ast_action_type) list -(* -let to_pat env = function - | AstListNode al -> let p,e = patl_of_astl env al in AstListPat p, e - | PureAstNode a -> let p,e = pat_of_ast env a in PureAstPat p, e -*) - let to_pat = pat_of_ast -(* - match ast with - | Node(_,"ASTPAT",[p]) -> pat_of_ast env p - | _ -> invalid_arg_loc (loc ast,"Ast.to_pat") -*) - - (* Substitution *) (* Locations in quoted ast are wrong (they refer to the right hand side of a grammar rule). A default location dloc is used whenever we create an ast constructor. Locations in the binding list are trusted. *) +(* For old ast printer *) let rec pat_sub dloc sigma pat = match pat with | Pmeta(pv,c) -> env_assoc sigma c (dloc,pv) @@ -549,6 +505,7 @@ and patl_sub dloc sigma pl = (* Converting and checking free meta-variables *) +(* For old ast printer *) let type_of_meta env loc pv = try List.assoc pv env @@ -556,6 +513,7 @@ let type_of_meta env loc pv = user_err_loc (loc,"Ast.type_of_meta", (str"variable " ++ str pv ++ str" is unbound")) +(* For old ast printer *) let check_ast_meta env loc pv = match type_of_meta env loc pv with | ETast -> () @@ -563,6 +521,7 @@ let check_ast_meta env loc pv = user_err_loc (loc,"Ast.check_ast_meta", (str"variable " ++ str pv ++ str" is not of ast type")) +(* For old ast printer *) let rec val_of_ast env = function | Nmeta(loc,pv) -> check_ast_meta env loc pv; @@ -593,48 +552,8 @@ and vall_of_astl env = function str"variable " ++ str pv ++ str" is not a List") | ast::asttl -> Pcons (val_of_ast env ast, vall_of_astl env asttl) | [] -> Pnil -(* -let rec val_of_ast_constr env = function -(* - | ConstrEval (r,c) -> ConstrEvalPat (r,val_of_ast_constr env c) - | ConstrContext (x,c) -> ConstrContextPat (x,val_of_ast_constr env c) -*) - | ConstrTerm c -> ConstrTermPat (val_of_ast env c) -*) -(* -let rec check_pat_meta env = function - | Pquote _ -> () - | Pmeta(s,Tany) -> check_ast_meta env loc s - | Pmeta(s,_) -> anomaly "not well-formed pattern" - | Pmeta_slam(s,b) -> - let _ = type_of_meta env loc s in (* ids are coerced to id lists *) - check_pat_meta env b - | Pslam(_,b) -> check_pat_meta env b - | Pnode(op,Plmeta (locv,pv)) -> - if type_of_meta env locv pv <> ETastl then - user_err_loc (locv,"Ast.vall_of_astl", - [< 'sTR"variable "; 'sTR pv; 'sTR" is not a List" >]) - | Pnode(op,l) -> check_patlist_meta env l - -and check_patlist_meta env = function - | Plmeta (locv,pv) -> - if type_of_meta env locv pv <> ETastl then - user_err_loc (locv,"Ast.vall_of_astl", - [< 'sTR"variable "; 'sTR pv; 'sTR" is not a List" >]) - | Pcons(Pmeta(pv,Tlist),l) -> - if l = Pnil then anomaly "not well-formed pattern list"; - if type_of_meta env locv pv <> ETastl then - user_err_loc (locv,"Ast.vall_of_astl", - [< 'sTR"variable "; 'sTR pv; 'sTR" is not a List" >]) - else check_patlist_meta env l - | Pcons(p,l) -> check_pat_meta env p; check_patlist_meta env l - | Pnil -> () - -let check_typed_pat_meta env = function - | AstListPat cl -> check_patlist_meta env cl - | PureAstPat c -> check_pat_meta env c -*) +(* For old ast printer *) let rec occur_var_ast s = function | Node(_,"QUALID",_::_::_) -> false | Node(_,"QUALID",[Nvar(_,s2)]) -> s = s2 @@ -645,104 +564,9 @@ let rec occur_var_ast s = function | Id _ | Str _ | Num _ | Path _ -> false | Dynamic _ -> (* Hum... what to do here *) false -let rec replace_vars_ast l = function - | Node(loc,op,args) -> Node (loc,op, List.map (replace_vars_ast l) args) - | Nvar(loc,s) as a -> (try Nvar (loc, List.assoc s l) with Not_found -> a) - | Smetalam _ | Nmeta _ -> anomaly "replace_var: metas should not occur here" - | Slam(loc,None,body) -> Slam(loc,None,replace_vars_ast l body) - | Slam(loc,Some s,body) as a -> - if List.mem_assoc s l then a else - Slam(loc,Some s,replace_vars_ast l body) - | Id _ | Str _ | Num _ | Path _ as a -> a - | Dynamic _ as a -> (* Hum... what to do here *) a - -(* Ast with cases and metavariables *) - -let print_sig = function - | [] -> - mt () - | sigma -> - str"with constraints :" ++ brk(1,1) ++ - v 0 (prlist_with_sep pr_spc - (fun (x,v) -> str x ++ str" = " ++ hov 0 (print_val v)) - sigma) - -let case_failed loc sigma e pats = - user_err_loc - (loc,"Ast.eval_act", - str"Grammar case failure. The ast" ++ spc () ++ print_ast e ++ - spc () ++ str"does not match any of the patterns :" ++ - brk(1,1) ++ v 0 (prlist_with_sep pr_spc print_astpat pats) ++ fnl () ++ - print_sig sigma) - -let caselist_failed loc sigma el pats = - user_err_loc - (loc,"Ast.eval_act", - str"Grammar case failure. The ast list" ++ brk(1,1) ++ print_astl el ++ - spc () ++ str"does not match any of the patterns :" ++ - brk(1,1) ++ v 0 (prlist_with_sep pr_spc print_astlpat pats) ++ fnl () ++ - print_sig sigma) - -let myfst = function - | PureAstPat p, a -> p - | _ -> error "Expects a pure ast" - -let myfstl = function - | AstListPat p, a -> p - | _ -> error "Expects an ast list" - -let rec eval_act dloc sigma = function - | Act (AstListPat patl) -> AstListNode (patl_sub dloc sigma patl) - | Act (PureAstPat pat) -> PureAstNode (pat_sub dloc sigma pat) - | ActCase(e,ml) -> - (match eval_act dloc sigma e with - | (PureAstNode esub) -> - (match first_match myfst sigma esub ml with - | Some((_,a),sigma_pat) -> eval_act dloc sigma_pat a - | _ -> case_failed dloc sigma esub (List.map myfst ml)) - | _ -> grammar_type_error (dloc,"Ast.eval_act")) - | ActCaseList(e,ml) -> - (match eval_act dloc sigma e with - | AstListNode elsub -> - (match first_matchl myfstl sigma elsub ml with - | Some((_,a),sigma_pat) -> eval_act dloc sigma_pat a - | _ -> caselist_failed dloc sigma elsub (List.map myfstl ml)) - | _ -> grammar_type_error (dloc,"Ast.eval_act")) - -let val_of_typed_ast loc env = function - | ETast, PureAstNode c -> PureAstPat (val_of_ast env c) - | ETastl, AstListNode cl -> AstListPat (vall_of_astl env cl) - | (ETast|ETastl), _ -> - invalid_arg_loc (loc,"Ast.act_of_ast: ill-typed") - -(* TODO: case sur des variables uniquement -> pas de pb de conflit Ast/List *) -let rec act_of_ast vars etyp = function - | CaseAction (loc,a,atyp,cl) -> - let pa = act_of_ast vars atyp a in - (match atyp with - | ETastl -> - let acl = List.map (caselist vars etyp) cl in - ActCaseList (pa,acl) - | _ -> - let acl = List.map (case loc vars etyp) cl in - ActCase (pa,acl)) - | SimpleAction (loc,a) -> Act (val_of_typed_ast loc vars (etyp,a)) - -and case loc vars etyp = function - | [p],a -> - let (apl,penv) = pat_of_ast vars p in - let aa = act_of_ast penv etyp a in - (PureAstPat apl,aa) - | _ -> - user_err_loc - (loc, "Ast.case", str"case pattern for an ast should be a single ast") - -and caselist vars etyp (pl,a) = - let (apl,penv) = patl_of_astl vars pl in - let aa = act_of_ast penv etyp a in - (AstListPat apl,aa) -let to_act_check_vars = act_of_ast +(**********************************************************************) +(* Object substitution in modules *) let rec subst_astpat subst = function | Pquote a -> Pquote (subst_ast subst a) @@ -758,12 +582,3 @@ and subst_astpatlist subst = function let subst_pat subst = function | AstListPat pl -> AstListPat (subst_astpatlist subst pl) | PureAstPat p -> PureAstPat (subst_astpat subst p) - -let rec subst_act subst = function - | Act p -> Act (subst_pat subst p) - | ActCase (a,l) -> - ActCase (subst_act subst a, - List.map (fun (p,a) -> subst_pat subst p, subst_act subst a) l) - | ActCaseList (a,l) -> - ActCaseList (subst_act subst a, - List.map (fun (p,a) -> subst_pat subst p, subst_act subst a) l) |