diff options
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 106 |
1 files changed, 98 insertions, 8 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c8f79b8c5..5b1d2813b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -176,6 +176,11 @@ allowed in abbreviatable expressions" (* Pattern-matching rawconstr and aconstr *) +let rec adjust_scopes = function + | _,[] -> [] + | [],a::args -> (None,a) :: adjust_scopes ([],args) + | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args) + exception No_match let rec alpha_var id1 id2 = function @@ -186,12 +191,79 @@ let rec alpha_var id1 id2 = function let alpha_eq_val (x,y) = x = y +(* +let bind_env sc sigma var v = + try + let vvar,_ = List.assoc var sigma in + if alpha_eq_val (v,vvar) then sigma + else raise No_match + with Not_found -> + (* TODO: handle the case of multiple occs in different scopes *) + (var,(v,sc))::sigma + +let rec match_ sc alp metas sigma a1 a2 = match (a1,a2) with + | r1, AVar id2 when List.mem id2 metas -> bind_env sc sigma id2 r1 + | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma + | RRef (_,r1), ARef r2 when r1 = r2 -> sigma + | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma + | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 -> + let sigma = match_ sc alp metas sigma f1 f2 in + let l1 = match f1 with + | RRef (_,ref) -> adjust_scopes (Symbols.find_arguments_scope ref,l1) + | _ -> List.map (fun a -> (None,a)) l1 in + List.fold_left2 (fun sigma (sc,a) b -> match_ sc alp metas sigma a b) sigma l1 l2 + | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) -> + match_binders sc alp metas (match_type alp metas sigma t1 t2) b1 b2 na1 na2 + | RProd (_,na1,t1,b1), AProd (na2,t2,b2) -> + match_binders (Some Symbols.type_scope) alp metas (match_type alp metas sigma t1 t2) b1 b2 na1 na2 + | RLetIn (_,na1,t1,b1), AProd (na2,t2,b2) -> + match_binders sc alp metas (match_ sc alp metas sigma t1 t2) b1 b2 na1 na2 + | RCases (_,po1,tml1,eqnl1), ACases (po2,tml2,eqnl2) -> + let sigma = option_fold_left2 (match_type alp metas) sigma po1 po2 in + let sigma = List.fold_left2 (match_ sc alp metas) sigma tml1 tml2 in + List.fold_left2 (match_equations sc alp metas) sigma eqnl1 eqnl2 + | ROrderedCase (_,st,po1,c1,bl1), AOrderedCase (st2,po2,c2,bl2) -> + let sigma = option_fold_left2 (match_type alp metas) sigma po1 po2 in + array_fold_left2 (match_ sc alp metas) + (match_ sc alp metas sigma c1 c2) bl1 bl2 + | RCast(_,c1,t1), ACast(c2,t2) -> + match_type alp metas (match_ sc alp metas sigma c1 c2) t1 t2 + | RSort (_,s1), ASort s2 when s1 = s2 -> sigma + | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match + | a, AHole _ when not(Options.do_translate()) -> sigma + | RHole _, AHole _ -> sigma + | (RDynamic _ | RRec _ | REvar _), _ + | _,_ -> raise No_match + +and match_type x = match_ (Some Symbols.type_scope) x + +and match_binders sc alp metas sigma b1 b2 na1 na2 = match (na1,na2) with + | (na1,Name id2) when List.mem id2 metas -> + let sigma = + name_fold + (fun id sigma -> bind_env None sigma id2 (RVar (dummy_loc,id))) na1 sigma + in + match_ sc alp metas sigma b1 b2 + | (na1,na2) -> + let alp = + name_fold + (fun id1 -> name_fold (fun id2 alp -> (id1,id2)::alp) na2) na1 alp in + match_ sc alp metas sigma b1 b2 + +and match_equations sc alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = + if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then + match_ sc alp metas sigma rhs1 rhs2 + else raise No_match + +*) + let bind_env sigma var v = try let vvar = List.assoc var sigma in if alpha_eq_val (v,vvar) then sigma else raise No_match - with Not_found -> + with Not_found -> + (* TODO: handle the case of multiple occs in different scopes *) (var,v)::sigma let rec match_ alp metas sigma a1 a2 = match (a1,a2) with @@ -243,7 +315,21 @@ and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = type scope_name = string -type interpretation = (identifier * scope_name list) list * aconstr +type interpretation = + (identifier * (scope_name option * scope_name list)) list * aconstr + +(* +let match_aconstr sc c (metas_scl,pat) = + let subst = match_ sc [] (List.map fst metas_scl) [] c pat in + (* Reorder canonically the substitution *) + let find x subst = + try List.assoc x subst + with Not_found -> + (* Happens for binders bound to Anonymous *) + (* Find a better way to propagate Anonymous... *) + RVar (dummy_loc,x),None in + List.map (fun (x,scl) -> let (a,sc) = find x subst in (a,sc,scl)) metas_scl +*) let match_aconstr c (metas_scl,pat) = let subst = match_ [] (List.map fst metas_scl) [] c pat in @@ -263,6 +349,8 @@ type notation = string type explicitation = int +type proj_flag = bool (* [true] = is projection *) + type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier | CPatCstr of loc * reference * cases_pattern_expr list @@ -278,8 +366,9 @@ type constr_expr = | CProdN of loc * (name located list * constr_expr) list * constr_expr | CLambdaN of loc * (name located list * constr_expr) list * constr_expr | CLetIn of loc * name located * constr_expr * constr_expr - | CAppExpl of loc * reference * constr_expr list - | CApp of loc * constr_expr * (constr_expr * explicitation option) list + | CAppExpl of loc * (proj_flag * reference) * constr_expr list + | CApp of loc * (proj_flag * constr_expr) * + (constr_expr * explicitation option) list | CCases of loc * constr_expr option * constr_expr list * (loc * cases_pattern_expr list * constr_expr) list | COrderedCase of loc * case_style * constr_expr option * constr_expr @@ -345,9 +434,9 @@ let occur_var_constr_ref id = function let rec occur_var_constr_expr id = function | CRef r -> occur_var_constr_ref id r | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b - | CAppExpl (loc,r,l) -> + | CAppExpl (loc,(_,r),l) -> occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l - | CApp (loc,f,l) -> + | CApp (loc,(_,f),l) -> occur_var_constr_expr id f or List.exists (fun (a,_) -> occur_var_constr_expr id a) l | CProdN (_,l,b) -> occur_var_binders id b l @@ -372,7 +461,7 @@ and occur_var_binders id b = function let mkIdentC id = CRef (Ident (dummy_loc, id)) let mkRefC r = CRef r -let mkAppC (f,l) = CApp (dummy_loc, f, List.map (fun x -> (x,None)) l) +let mkAppC (f,l) = CApp (dummy_loc, (false,f), List.map (fun x -> (x,None)) l) let mkCastC (a,b) = CCast (dummy_loc,a,b) let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b) let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) @@ -389,7 +478,8 @@ let map_binders f g e bl = let map_constr_expr_with_binders f g e = function | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b) | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l) - | CApp (loc,a,l) -> CApp (loc,f e a,List.map (fun (a,i) -> (f e a,i)) l) + | CApp (loc,(p,a),l) -> + CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l) | CProdN (loc,bl,b) -> let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b) | CLambdaN (loc,bl,b) -> |