summaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml83
1 files changed, 46 insertions, 37 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index efb6c853..f99af68e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: constrextern.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
(*i*)
open Pp
@@ -190,8 +190,9 @@ let rec check_same_type ty1 ty2 =
check_same_type b1 b2
| CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
check_same_type a1 a2
- | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
- List.iter2 check_same_type e1 e2
+ | CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 ->
+ List.iter2 check_same_type e1 e2;
+ List.iter2 (List.iter2 check_same_type) el1 el2
| CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
| CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
check_same_type e1 e2
@@ -298,7 +299,7 @@ and spaces ntn n =
if n = String.length ntn then []
else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
-let expand_curly_brackets loc mknot ntn l =
+let expand_curly_brackets loc mknot ntn (l,ll) =
let ntn' = ref ntn in
let rec expand_ntn i =
function
@@ -311,12 +312,12 @@ let expand_curly_brackets loc mknot ntn l =
ntn' :=
String.sub !ntn' 0 p ^ "_" ^
String.sub !ntn' (p+5) (String.length !ntn' -p-5);
- mknot (loc,"{ _ }",[a]) end
+ mknot (loc,"{ _ }",([a],[])) end
else a in
a' :: expand_ntn (i+1) l in
let l = expand_ntn 0 l in
(* side effect *)
- mknot (loc,!ntn',l)
+ mknot (loc,!ntn',(l,ll))
let destPrim = function CPrim(_,t) -> Some t | _ -> None
let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
@@ -324,18 +325,18 @@ let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
let make_notation_gen loc ntn mknot mkprim destprim l =
if has_curly_brackets ntn
then expand_curly_brackets loc mknot ntn l
- else match ntn,List.map destprim l with
+ else match ntn,List.map destprim (fst l),(snd l) with
(* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
- | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
- mknot (loc,ntn,[mknot (loc,"( _ )",l)])
+ | "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p ->
+ mknot (loc,ntn,([mknot (loc,"( _ )",l)],[]))
| _ ->
match decompose_notation_key ntn, l with
- | [Terminal "-"; Terminal x], [] ->
+ | [Terminal "-"; Terminal x], ([],[]) ->
(try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
- with _ -> mknot (loc,ntn,[]))
- | [Terminal x], [] ->
+ with _ -> mknot (loc,ntn,([],[])))
+ | [Terminal x], ([],[]) ->
(try mkprim (loc, Numeral (Bigint.of_string x))
- with _ -> mknot (loc,ntn,[]))
+ with _ -> mknot (loc,ntn,([],[])))
| _ ->
mknot (loc,ntn,l)
@@ -351,13 +352,13 @@ let make_pat_notation loc ntn l =
(fun (loc,p) -> CPatPrim (loc,p))
destPatPrim l
-let bind_env sigma var v =
+let bind_env (sigma,sigmalist as fullsigma) var v =
try
let vvar = List.assoc var sigma in
- if v=vvar then sigma else raise No_match
+ if v=vvar then fullsigma else raise No_match
with Not_found ->
(* TODO: handle the case of multiple occs in different scopes *)
- (var,v)::sigma
+ (var,v)::sigma,sigmalist
let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
| r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
@@ -378,15 +379,18 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
(* All parameters must be _ *)
List.iter (function AHole _ -> () | _ -> raise No_match) p2;
List.fold_left2 (match_cases_pattern metas) sigma args1 args2
+ (* TODO: use recursive notations *)
| _ -> raise No_match
-let match_aconstr_cases_pattern c (metas_scl,pat) =
- let subst = match_cases_pattern (List.map fst metas_scl) [] c pat in
+let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
+ let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
+ let subst,substlist = match_cases_pattern vars ([],[]) c pat in
(* Reorder canonically the substitution *)
let find x subst =
- try List.assoc x subst
+ try List.assoc x subst
with Not_found -> anomaly "match_aconstr_cases_pattern" in
- List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
+ List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
+ List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
(* Better to use extern_rawconstr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
@@ -424,7 +428,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| PatCstr (loc,_,_,na),_ -> loc,na
| PatVar (loc,na),_ -> loc,na in
(* Try matching ... *)
- let subst = match_aconstr_cases_pattern t pat in
+ let subst,substlist = match_aconstr_cases_pattern t pat in
(* Try availability of interpretation ... *)
let p = match keyrule with
| NotationRule (sc,ntn) ->
@@ -438,7 +442,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
List.map (fun (c,(scopt,scl)) ->
extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
subst in
- insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
+ let ll =
+ List.map (fun (c,(scopt,scl)) ->
+ let subscope = (scopt,scl@scopes') in
+ List.map (extern_cases_pattern_in_scope subscope vars) c)
+ substlist in
+ insert_pat_delimiters loc
+ (make_pat_notation loc ntn (l,ll)) key)
| SynDefRule kn ->
let qid = shortest_qualid_of_syndef vars kn in
CPatAtom (loc,Some (Qualid (loc, qid))) in
@@ -544,15 +554,10 @@ let rec remove_coercions inctx = function
(* We skip a coercion *)
let l = list_skipn n args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
- let (a,l) =
- (* Recursively remove the head coercions *)
- match remove_coercions true a with
- | RApp (_,a,l') -> a,l'@l
- | a -> a,l in
- if l = [] then a
- else
- (* Recursively remove coercions in arguments *)
- RApp (loc,a,List.map (remove_coercions true) l)
+ (* Recursively remove the head coercions *)
+ (match remove_coercions true a with
+ | RApp (_,a,l') -> RApp (loc,a,l'@l)
+ | a -> RApp (loc,a,l))
| _ -> c
with Not_found -> c)
| c -> c
@@ -671,7 +676,7 @@ let rec extern inctx scopes vars r =
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
-
+
| RCases (loc,sty,rtntypopt,tml,eqns) ->
let vars' =
List.fold_right (name_fold Idset.add)
@@ -694,7 +699,7 @@ let rec extern inctx scopes vars r =
| Name id -> RVar (dummy_loc,id)) nal in
let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
(extern_typ scopes vars t)) x))) tml in
- let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in
+ let eqns = List.map (extern_eqn inctx scopes vars) eqns in
CCases (loc,sty,rtntypopt',tml,eqns)
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
@@ -702,13 +707,13 @@ let rec extern inctx scopes vars r =
(Option.map (fun _ -> na) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
- extern false scopes (List.fold_left add_vname vars nal) b)
+ extern inctx scopes (List.fold_left add_vname vars nal) b)
| RIf (loc,c,(na,typopt),b1,b2) ->
CIf (loc,sub_extern false scopes vars c,
(Option.map (fun _ -> na) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
- sub_extern false scopes vars b1, sub_extern false scopes vars b2)
+ sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
| RRec (loc,fk,idv,blv,tyv,bv) ->
let vars' = Array.fold_right Idset.add idv vars in
@@ -822,7 +827,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
| _, None -> t,[]
| _ -> raise No_match in
(* Try matching ... *)
- let subst = match_aconstr t pat in
+ let subst,substlist = match_aconstr t pat in
(* Try availability of interpretation ... *)
let e =
match keyrule with
@@ -838,7 +843,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
extern (* assuming no overloading: *) true
(scopt,scl@scopes') vars c)
subst in
- insert_delimiters (make_notation loc ntn l) key)
+ let ll =
+ List.map (fun (c,(scopt,scl)) ->
+ List.map (extern true (scopt,scl@scopes') vars) c)
+ substlist in
+ insert_delimiters (make_notation loc ntn (l,ll)) key)
| SynDefRule kn ->
let l =
List.map (fun (c,(scopt,scl)) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-25 19:18:05 +0000