diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 14:23:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | 158f40db9482ead89befbf9bc9ad45ff8a60b75f (patch) | |
| tree | 92587db07ddf50e2db16b270966115fa3d66d64a /interp/notation.ml | |
| parent | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (diff) | |
[location] Switch glob_constr to Loc.located
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index aef089299..3bcec3001 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -264,12 +264,12 @@ let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) let prim_token_key_table = ref KeyMap.empty let glob_prim_constr_key = function - | GApp (_,GRef (_,ref,_),_) | GRef (_,ref,_) -> RefKey (canonical_gr ref) + | _, GApp ((_, GRef (ref,_)),_) | _, GRef (ref,_) -> RefKey (canonical_gr ref) | _ -> Oth let glob_constr_keys = function - | GApp (_,GRef (_,ref,_),_) -> [RefKey (canonical_gr ref); Oth] - | GRef (_,ref,_) -> [RefKey (canonical_gr ref)] + | _, GApp ((_, GRef (ref,_)),_) -> [RefKey (canonical_gr ref); Oth] + | _, GRef (ref,_) -> [RefKey (canonical_gr ref)] | _ -> [Oth] let cases_pattern_key = function @@ -471,13 +471,14 @@ let interp_prim_token = (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) -let rec rcp_of_glob looked_for = function - | GVar (loc,id) -> Loc.tag ~loc @@ RCPatAtom (Some id) - | GHole (loc,_,_,_) -> Loc.tag ~loc @@ RCPatAtom (None) - | GRef (loc,g,_) -> looked_for g; Loc.tag ~loc @@ RCPatCstr (g,[],[]) - | GApp (loc,GRef (_,g,_),l) -> - looked_for g; Loc.tag ~loc @@ RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[]) +let rec rcp_of_glob looked_for gt = Loc.map (function + | GVar id -> RCPatAtom (Some id) + | GHole (_,_,_) -> RCPatAtom None + | GRef (g,_) -> looked_for g; RCPatCstr (g,[],[]) + | GApp ((_, GRef (g,_)),l) -> + looked_for g; RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[]) | _ -> raise Not_found + ) gt let interp_prim_token_cases_pattern_expr loc looked_for p = interp_prim_token_gen (rcp_of_glob looked_for) loc p @@ -521,8 +522,8 @@ let uninterp_prim_token_ind_pattern ind args = if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = GRef (Loc.ghost,ref,None) in - match numpr (GApp (Loc.ghost,ref,args')) with + let ref = Loc.tag @@ GRef (ref,None) in + match numpr (Loc.tag @@ GApp (ref,args')) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) with Not_found -> raise Notation_ops.No_match |