diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 193 | ||||
| -rw-r--r-- | interp/constrextern.mli | 1 | ||||
| -rw-r--r-- | interp/constrintern.ml | 54 | ||||
| -rw-r--r-- | interp/reserve.ml | 10 | ||||
| -rw-r--r-- | interp/topconstr.ml | 101 | ||||
| -rw-r--r-- | interp/topconstr.mli | 11 |
6 files changed, 303 insertions, 67 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1027543847..29f3c437c5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -103,8 +103,8 @@ let idopt_of_name = function | Anonymous -> None let extern_evar loc n = - warning - "Existential variable turned into meta-variable during externalization"; + msgerrnl (str + "Warning: existential variable turned into meta-variable during externalization"); CPatVar (loc,(false,make_ident "META" (Some n))) let raw_string_of_ref = function @@ -120,6 +120,15 @@ let raw_string_of_ref = function (* v7->v8 translation *) +let translate_keyword = function + | ("forall" | "fun" | "match" | "fix" | "cofix" | "for" | "let" + | "if" | "then" | "else" | "return" as s) -> + let s' = s^"_" in + msgerrnl + (str ("Warning: "^s^" is now a keyword; it has been translated to "^s')); + s' + | s -> s + let is_coq_root d = let d = repr_dirpath d in d <> [] & string_of_id (list_last d) = "Coq" @@ -174,6 +183,7 @@ let translate_v7_string = function | "fact_growing" -> "fact_le" (* Lists *) | "idempot_rev" -> "involutive_rev" + | "forall" -> "HereAndFurther" (* Bool *) | "orb_sym" -> "orb_comm" | "andb_sym" -> "andb_comm" @@ -192,9 +202,13 @@ let id_of_v7_string s = id_of_string (if !Options.v7 then s else translate_v7_string s) let v7_to_v8_dir_id dir id = - if Options.do_translate() - & (is_coq_root (Lib.library_dp()) or is_coq_root dir) - then id_of_string (translate_v7_string (string_of_id id)) else id + if Options.do_translate() then + let s = string_of_id id in + let s = + if (is_coq_root (Lib.library_dp()) or is_coq_root dir) + then translate_v7_string s else s in + id_of_string (translate_keyword s) + else id let v7_to_v8_id = v7_to_v8_dir_id empty_dirpath @@ -209,6 +223,90 @@ let extern_reference loc vars r = (* happens in debugger *) Ident (loc,id_of_string (raw_string_of_ref r)) +(***********************************************************************) +(* Equality up to location (useful for translator v8) *) + +let rec check_same_pattern p1 p2 = + match p1, p2 with + | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 -> + check_same_pattern a1 a2 + | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 -> + List.iter2 check_same_pattern a1 a2 + | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> () + | CPatNumeral(_,i1), CPatNumeral(_,i2) when i1=i2 -> () + | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 -> + check_same_pattern e1 e2 + | _ -> failwith "not same pattern" + +let check_same_ref r1 r2 = + match r1,r2 with + | Qualid(_,q1), Qualid(_,q2) when q1=q2 -> () + | Ident(_,i1), Ident(_,i2) when i1=i2 -> () + | _ -> failwith "not same ref" + +let rec check_same_type ty1 ty2 = + match ty1, ty2 with + | CRef r1, CRef r2 -> check_same_ref r1 r2 + | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 -> + List.iter2 (fun (id1,i1,a1,b1) (id2,i2,a2,b2) -> + if id1<>id2 || i1<>i2 then failwith "not same fix"; + check_same_type a1 a2; + check_same_type b1 b2) + fl1 fl2 + | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 -> + List.iter2 (fun (id1,a1,b1) (id2,a2,b2) -> + if id1<>id2 then failwith "not same fix"; + check_same_type a1 a2; + check_same_type b1 b2) + fl1 fl2 + | CArrow(_,a1,b1), CArrow(_,a2,b2) -> + check_same_type a1 a2; + check_same_type b1 b2 + | CProdN(_,bl1,a1), CProdN(_,bl2,a2) -> + List.iter2 check_same_binder bl1 bl2; + check_same_type a1 a2 + | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> + List.iter2 check_same_binder bl1 bl2; + check_same_type a1 a2 + | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 -> + check_same_type a1 a2; + check_same_type b1 b2 + | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 -> + List.iter2 check_same_type al1 al2 + | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) -> + check_same_type e1 e2; + List.iter2 (fun (a1,e1) (a2,e2) -> + if e1<>e2 then failwith "not same expl"; + check_same_type a1 a2) al1 al2 + | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) -> + List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; + List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> + List.iter2 check_same_pattern pl1 pl2; + check_same_type r1 r2) brl1 brl2 + | COrderedCase(_,_,_,a1,bl1), COrderedCase(_,_,_,a2,bl2) -> + check_same_type a1 a2; + List.iter2 check_same_type bl1 bl2 + | CHole _, CHole _ -> () + | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () + | CSort(_,s1), CSort(_,s2) when s1=s2 -> () + | CCast(_,a1,b1), CCast(_,a2,b2) -> + check_same_type a1 a2; + check_same_type b1 b2 + | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 -> + List.iter2 check_same_type e1 e2 + | CNumeral(_,i1), CNumeral(_,i2) when i1=i2 -> () + | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 -> + check_same_type e1 e2 + | _ when ty1=ty2 -> () + | _ -> failwith "not same type" + +and check_same_binder (nal1,e1) (nal2,e2) = + List.iter2 (fun (_,na1) (_,na2) -> + if na1<>na2 then failwith "not same name") nal1 nal2; + check_same_type e1 e2 + +let same c d = try check_same_type c d; true with _ -> false + (**********************************************************************) (* conversion of terms and cases patterns *) @@ -225,14 +323,14 @@ let rec extern_cases_pattern_in_scope scopes vars pat = insert_pat_delimiters (CPatNumeral (loc,n)) key with No_match -> match pat with - | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id))) + | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,v7_to_v8_id id))) | PatVar (loc,Anonymous) -> CPatAtom (loc, None) | PatCstr(loc,cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = CPatCstr (loc,extern_reference loc vars (ConstructRef cstrsp),args) in (match na with - | Name id -> CPatAlias (loc,p,id) + | Name id -> CPatAlias (loc,p,v7_to_v8_id id) | Anonymous -> p) let occur_name na aty = @@ -241,12 +339,21 @@ let occur_name na aty = | Anonymous -> false let is_projection nargs = function + | Some r -> + (try + let n = Recordops.find_projection_nparams r + 1 in + if n <= nargs then Some n else None + with Not_found -> None) + | None -> None + +let stdlib = function | Some r -> - (try Recordops.find_projection_nparams r + 1 = nargs - with Not_found -> false) - | None -> - false - + let dir,id = repr_path (sp_of_global r) in + (is_coq_root (Lib.library_dp()) or is_coq_root dir) + && not (List.mem (string_of_id id) + ["Zlength";"Zlength_correct";"eq_ind"]) + | None -> false + (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) let explicitize loc inctx impl (cf,f) args = @@ -256,16 +363,27 @@ let explicitize loc inctx impl (cf,f) args = let tail = exprec (q+1) (args,impl) in let visible = (!print_implicits & !print_implicits_explicit_args) - or not (is_inferable_implicit inctx n imp) - or ((match a with CHole _ -> false | _ -> true) - & Options.do_translate()) in + or (not (is_inferable_implicit inctx n imp)) + or ((match a with CHole _ -> false | _ -> true) + & Options.do_translate() & not (stdlib cf)) in if visible then (a,Some q) :: tail else tail | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl) | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) | [], _ -> [] in - let isproj = is_projection (List.length args) cf in - let args = exprec 1 (args,impl) in - if args = [] then f else CApp (loc, (isproj, f), args) + match is_projection (List.length args) cf with + | Some i as ip -> + if impl <> [] & is_status_implicit (List.nth impl (i-1)) then + let f' = match f with CRef f -> f | _ -> assert false in + CAppExpl (loc,(ip,f'),args) + else + let (args1,args2) = list_chop i args in + let (impl1,impl2) = if impl=[] then [],[] else list_chop i impl in + let args1 = exprec 1 (args1,impl1) in + let args2 = exprec (i+1) (args2,impl2) in + CApp (loc,(Some (List.length args1),f),args1@args2) + | None -> + let args = exprec 1 (args,impl) in + if args = [] then f else CApp (loc, (None, f), args) let rec skip_coercion dest_ref (f,args as app) = if !print_coercions or Options.do_translate () then app @@ -362,19 +480,35 @@ let rec extern inctx scopes vars r = let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,t],c) - | RCases (loc,typopt,tml,eqns) -> + | RCases (loc,(typopt,rtntypopt),tml,eqns) -> let pred = option_app (extern_type scopes vars) typopt in - let tml = List.map (extern false scopes vars) tml in + let rtntypopt = option_app (extern_type scopes vars) !rtntypopt in + let vars' = + List.fold_right (name_fold Idset.add) + (cases_predicate_names tml) vars in + let tml = List.map (fun (tm,{contents=(na,x)}) -> + (extern false scopes vars tm, + (na,option_app (fun (loc,ind,nal) -> + (loc,extern_reference loc vars (IndRef ind),nal)) x))) tml in let eqns = List.map (extern_eqn (typopt<>None) scopes vars) eqns in - CCases (loc,pred,tml,eqns) - - | ROrderedCase (loc,cs,typopt,tm,bv) -> + CCases (loc,(pred,rtntypopt),tml,eqns) + + | ROrderedCase (loc,cs,typopt,tm,bv,{contents = Some x}) -> + extern false scopes vars x + + | ROrderedCase (loc,cs,typopt,tm,bv,_) -> let bv = Array.to_list (Array.map (extern (typopt<>None) scopes vars) bv) in COrderedCase (loc,cs,option_app (extern_type scopes vars) typopt, extern false scopes vars tm,bv) + | RLetTuple (loc,nal,(na,typopt),tm,b) -> + CLetTuple (loc,nal, + (na,option_app (extern_type scopes (add_vname vars na)) typopt), + extern false scopes vars tm, + extern false scopes (List.fold_left add_vname vars nal) b) + | RRec (loc,fk,idv,tyv,bv) -> let vars' = Array.fold_right Idset.add idv vars in (match fk with @@ -411,7 +545,7 @@ and extern_type (_,scopes) = extern true (Some Symbols.type_scope,scopes) and factorize_prod scopes vars aty = function | RProd (loc,(Name id as na),ty,c) - when aty = extern true scopes vars (anonymize_if_reserved na ty) + when same aty (extern true scopes vars (anonymize_if_reserved na ty)) & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *) -> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in ((loc,Name id)::nal,c) @@ -419,7 +553,7 @@ and factorize_prod scopes vars aty = function and factorize_lambda inctx scopes vars aty = function | RLambda (loc,na,ty,c) - when aty = extern inctx scopes vars (anonymize_if_reserved na ty) + when same aty (extern inctx scopes vars (anonymize_if_reserved na ty)) & not (occur_name na aty) (* To avoid na in ty' escapes scope *) -> let (nal,c) = factorize_lambda inctx scopes (add_vname vars na) aty c in @@ -521,16 +655,17 @@ let rec raw_of_pat tenv env = function RLambda (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) | PCase ((_,(IfStyle|LetStyle as cs)),typopt,tm,bv) -> ROrderedCase (loc,cs,option_app (raw_of_pat tenv env) typopt, - raw_of_pat tenv env tm,Array.map (raw_of_pat tenv env) bv) + raw_of_pat tenv env tm,Array.map (raw_of_pat tenv env) bv, ref None) | PCase ((_,cs),typopt,tm,[||]) -> - RCases (loc,option_app (raw_of_pat tenv env) typopt, - [raw_of_pat tenv env tm],[]) + RCases (loc,(option_app (raw_of_pat tenv env) typopt,ref None (* TODO *)), + [raw_of_pat tenv env tm,ref (Anonymous,None)],[]) | PCase ((Some ind,cs),typopt,tm,bv) -> let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in + let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in Detyping.detype_case false (fun tenv _ -> raw_of_pat tenv) (fun tenv _ -> raw_of_eqn tenv) - tenv avoid env ind cs typopt tm bv + tenv avoid env ind cs typopt k tm bv | PCase _ -> error "Unsupported case-analysis while printing pattern" | PFix f -> Detyping.detype tenv [] env (mkFix f) | PCoFix c -> Detyping.detype tenv [] env (mkCoFix c) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index e5cfd0190f..008957e1bb 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -26,6 +26,7 @@ open Symbols val id_of_v7_string : string -> identifier val v7_to_v8_id : identifier -> identifier (* v7->v8 translation *) val shortest_qualid_of_v7_global : Idset.t -> global_reference -> qualid +val check_same_type : constr_expr -> constr_expr -> unit (* Translation of pattern, cases pattern, rawterm and term into syntax trees for printing *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 17405769a5..d1c32e9982 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -178,6 +178,20 @@ let intern_qualid loc qid = with Not_found -> error_global_not_found_loc loc qid +let intern_inductive r = + let loc,qid = qualid_of_reference r in + try match Nametab.extended_locate qid with + | TrueGlobal (IndRef ind) -> ind, [] + | TrueGlobal _ -> raise Not_found + | SyntacticDef sp -> + (match Syntax_def.search_syntactic_definition loc sp with + | RApp (_,RRef(_,IndRef ind),l) + when List.for_all (function RHole _ -> true | _ -> false) l -> + (ind, List.map (fun _ -> Anonymous) l) + | _ -> raise Not_found) + with Not_found -> + error_global_not_found_loc loc qid + let intern_reference env lvar = function | Qualid (loc, qid) -> intern_qualid loc qid @@ -373,20 +387,26 @@ let locate_if_isevar loc na = function with Not_found -> RHole (loc, BinderType na)) | x -> x +let push_name_env (ids,impls,tmpsc,scopes as env) = function + | Anonymous -> env + | Name id -> (Idset.add id ids,impls,tmpsc,scopes) + (**********************************************************************) (* Utilities for application *) -let check_projection nargs = function - | RRef (loc, ref) -> +let check_projection isproj nargs r = + match (r,isproj) with + | RRef (loc, ref), Some nth -> (try let n = Recordops.find_projection_nparams ref in - if nargs <> n+1 then + if nargs < nth then user_err_loc (loc,"",str "Projection has not enough parameters"); with Not_found -> user_err_loc (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection")) - | r -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection") + | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection") + | _, None -> () let set_hole_implicit i = function | RRef (loc,r) -> (loc,ImplicitArg (r,i)) @@ -498,7 +518,7 @@ let internalise sigma env allow_soapp lvar c = intern (ids,impls,None,find_delimiters_scope loc key::scopes) e | CAppExpl (loc, (isproj,ref), args) -> let (f,_,args_scopes) = intern_reference env lvar ref in - if isproj then check_projection (List.length args) f; + check_projection isproj (List.length args) f; RApp (loc, f, intern_args env args_scopes args) | CApp (loc, (isproj,f), args) -> let (c, impargs, args_scopes) = @@ -507,20 +527,34 @@ let internalise sigma env allow_soapp lvar c = | _ -> (intern env f, [], []) in let args = intern_impargs c env impargs args_scopes args in - if isproj then check_projection (List.length args) c; + check_projection isproj (List.length args) c; (match c with | RApp (loc', f', args') -> (* May happen with the ``...`` and `...` grammars *) RApp (join_loc loc' loc, f',args'@args) | _ -> RApp (loc, c, args)) - | CCases (loc, po, tms, eqns) -> - RCases (loc, option_app (intern_type env) po, - List.map (intern env) tms, + | CCases (loc, (po,rtnpo), tms, eqns) -> + let rtnids = List.fold_right (fun (_,(na,x)) ids -> + let ids = match x with + | Some (_,_,nal) -> List.fold_right (name_fold Idset.add) nal ids + | _ -> ids in + name_fold Idset.add na ids) tms ids in + let rtnpo = + option_app (intern_type (rtnids,impls,tmp_scope,scopes)) rtnpo in + RCases (loc, (option_app (intern_type env) po, ref rtnpo), + List.map (fun (tm,(na,indnalo)) -> + (intern env tm,ref (na,option_app (fun (loc,r,nal) -> + let ind,l = intern_inductive r in + (loc,ind,l@nal)) indnalo))) tms, List.map (intern_eqn (List.length tms) env) eqns) | COrderedCase (loc, tag, po, c, cl) -> ROrderedCase (loc, tag, option_app (intern_type env) po, intern env c, - Array.of_list (List.map (intern env) cl)) + Array.of_list (List.map (intern env) cl),ref None) + | CLetTuple (loc, nal, (na,po), b, c) -> + RLetTuple (loc, nal, + (na, option_app (intern_type (push_name_env env na)) po), + intern env b, intern (List.fold_left push_name_env env nal) c) | CHole loc -> RHole (loc, QuestionMark) | CPatVar (loc, n) when allow_soapp -> diff --git a/interp/reserve.ml b/interp/reserve.ml index f6f9fe60d3..5287ce5a2d 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -43,12 +43,14 @@ let rec unloc = function | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c) | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c) | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RCases (_,tyopt,tml,pl) -> - RCases (dummy_loc,option_app unloc tyopt,List.map unloc tml, + | RCases (_,(tyopt,rtntypopt),tml,pl) -> + RCases (dummy_loc, + (option_app unloc tyopt,ref (option_app unloc !rtntypopt)), + List.map (fun (tm,x) -> (unloc tm,x)) tml, List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) - | ROrderedCase (_,b,tyopt,tm,bv) -> + | ROrderedCase (_,b,tyopt,tm,bv,x) -> ROrderedCase - (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv) + (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv,x) | RRec (_,fk,idl,tyl,bv) -> RRec (dummy_loc,fk,idl,Array.map unloc tyl,Array.map unloc bv) | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 5b1d2813b4..d2ef146bf2 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -28,9 +28,11 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ACases of aconstr option * aconstr list * + | ACases of aconstr option * aconstr option * + (aconstr * (name * (inductive * name list) option)) list * (identifier list * cases_pattern list * aconstr) list | AOrderedCase of case_style * aconstr option * aconstr * aconstr array + | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | ASort of rawsort | AHole of hole_kind | APatVar of patvar @@ -49,13 +51,24 @@ let map_aconstr_with_binders_loc loc g f e = function let na,e = name_app g e na in RProd (loc,na,f e ty,f e c) | ALetIn (na,b,c) -> let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c) - | ACases (tyopt,tml,eqnl) -> + | ACases (tyopt,rtntypopt,tml,eqnl) -> + let cases_predicate_names tml = + List.flatten (List.map (function + | (tm,(na,None)) -> [na] + | (tm,(na,Some (_,nal))) -> na::nal) tml) in + (* TODO: apply g to na (in fact not used) *) + let e' = List.fold_right + (fun na e -> snd (name_app g e na)) (cases_predicate_names tml) e in let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in let eqnl = List.map (fun (idl,pat,rhs) -> let (idl,e) = List.fold_right fold idl ([],e) in (loc,idl,pat,f e rhs)) eqnl in - RCases (loc,option_app (f e) tyopt,List.map (f e) tml,eqnl) + RCases (loc,(option_app (f e) tyopt, ref (option_app (f e') rtntypopt)), + List.map (fun (tm,(na,x)) -> + (f e tm,ref (na,option_app (fun (x,y) -> (loc,x,y)) x))) tml,eqnl) | AOrderedCase (b,tyopt,tm,bv) -> - ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv) + ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv,ref None) + | ALetTuple (nal,(na,po),b,c) -> + RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c) | ACast (c,t) -> RCast (loc,f e c,f e t) | ASort x -> RSort (loc,x) | AHole x -> RHole (loc,x) @@ -101,9 +114,17 @@ let rec subst_aconstr subst raw = if r1' == r1 && r2' == r2 then raw else ALetIn (n,r1',r2') - | ACases (ro,rl,branches) -> + | ACases (ro,rtntypopt,rl,branches) -> let ro' = option_smartmap (subst_aconstr subst) ro - and rl' = list_smartmap (subst_aconstr subst) rl + and rtntypopt' = option_smartmap (subst_aconstr subst) rtntypopt + and rl' = list_smartmap + (fun (a,(n,signopt) as x) -> + let a' = subst_aconstr subst a in + let signopt' = option_app (fun ((indkn,i),nal as z) -> + let indkn' = subst_kn subst indkn in + if indkn == indkn' then z else ((indkn',i),nal)) signopt in + if a' == a && signopt' == signopt then x else (a',(n,signopt'))) + rl and branches' = list_smartmap (fun (idl,cpl,r as branch) -> let cpl' = list_smartmap (subst_pat subst) cpl @@ -112,8 +133,9 @@ let rec subst_aconstr subst raw = (idl,cpl',r')) branches in - if ro' == ro && rl' == rl && branches' == branches then raw else - ACases (ro',rl',branches') + if ro' == ro && rtntypopt == rtntypopt' & + rl' == rl && branches' == branches then raw else + ACases (ro',rtntypopt',rl',branches') | AOrderedCase (b,ro,r,ra) -> let ro' = option_smartmap (subst_aconstr subst) ro @@ -122,6 +144,13 @@ let rec subst_aconstr subst raw = if ro' == ro && r' == r && ra' == ra then raw else AOrderedCase (b,ro',r',ra') + | ALetTuple (nal,(na,po),b,c) -> + let po' = option_smartmap (subst_aconstr subst) po + and b' = subst_aconstr subst b + and c' = subst_aconstr subst c in + if po' == po && b' == b && c' == c then raw else + ALetTuple (nal,(na,po'),b',c') + | APatVar _ | ASort _ -> raw | AHole (ImplicitArg (ref,i)) -> @@ -151,13 +180,22 @@ let aconstr_of_rawconstr vars a = | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c) | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c) | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c) - | RCases (_,tyopt,tml,eqnl) -> + | RCases (_,(tyopt,rtntypopt),tml,eqnl) -> let f (_,idl,pat,rhs) = bound_binders := idl@(!bound_binders); (idl,pat,aux rhs) in - ACases (option_app aux tyopt,List.map aux tml, List.map f eqnl) - | ROrderedCase (_,b,tyopt,tm,bv) -> + ACases (option_app aux tyopt, + option_app aux !rtntypopt, + List.map (fun (tm,{contents = (na,x)}) -> + add_name bound_binders na; + option_iter + (fun (_,_,nl) -> List.iter (add_name bound_binders) nl) x; + (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml, + List.map f eqnl) + | ROrderedCase (_,b,tyopt,tm,bv,_) -> AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv) + | RLetTuple (loc,nal,(na,po),b,c) -> + ALetTuple (nal,(na,option_app aux po),aux b,aux c) | RCast (_,c,t) -> ACast (aux c,aux t) | RSort (_,s) -> ASort s | RHole (_,w) -> AHole w @@ -279,11 +317,13 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2 | RLetIn (_,na1,t1,b1), AProd (na2,t2,b2) -> match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2 - | RCases (_,po1,tml1,eqnl1), ACases (po2,tml2,eqnl2) -> + | RCases (_,(po1,rtno1),tml1,eqnl1), ACases (po2,rtno2,tml2,eqnl2) -> let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in - let sigma = List.fold_left2 (match_ alp metas) sigma tml1 tml2 in + (* TODO: match rtno' with their contexts *) + let sigma = List.fold_left2 + (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2 - | ROrderedCase (_,st,po1,c1,bl1), AOrderedCase (st2,po2,c2,bl2) -> + | ROrderedCase (_,st,po1,c1,bl1,_), AOrderedCase (st2,po2,c2,bl2) -> let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in array_fold_left2 (match_ alp metas) (match_ alp metas sigma c1 c2) bl1 bl2 | RCast(_,c1,t1), ACast(c2,t2) -> @@ -349,7 +389,7 @@ type notation = string type explicitation = int -type proj_flag = bool (* [true] = is projection *) +type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier @@ -369,10 +409,13 @@ type constr_expr = | 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 * + | CCases of loc * (constr_expr option * constr_expr option) * + (constr_expr * (name * (loc * reference * name list) option)) list * (loc * cases_pattern_expr list * constr_expr) list | COrderedCase of loc * case_style * constr_expr option * constr_expr * constr_expr list + | CLetTuple of loc * name list * (name * constr_expr option) * + constr_expr * constr_expr | CHole of loc | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key @@ -410,6 +453,7 @@ let constr_loc = function | CApp (loc,_,_) -> loc | CCases (loc,_,_,_) -> loc | COrderedCase (loc,_,_,_,_) -> loc + | CLetTuple (loc,_,_,_,_) -> loc | CHole loc -> loc | CPatVar (loc,_) -> loc | CEvar (loc,_) -> loc @@ -448,6 +492,7 @@ let rec occur_var_constr_expr id = function | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false | CCases (loc,_,_,_) | COrderedCase (loc,_,_,_,_) + | CLetTuple (loc,_,_,_,_) | CFix (loc,_,_) | CCoFix (loc,_,_) -> Pp.warning "Capture check in multiple binders not done"; false @@ -461,7 +506,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, (false,f), List.map (fun x -> (x,None)) l) +let mkAppC (f,l) = CApp (dummy_loc, (None,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) @@ -469,10 +514,11 @@ let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b) (* Used in correctness and interface *) +let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e + let map_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (nal,t) (e,bl) = - (List.fold_right (fun (_,na) -> name_fold g na) nal e,(nal,f e t)::bl) in + let h (nal,t) (e,bl) = (map_binder g e nal,(nal,f e t)::bl) in List.fold_right h bl (e,[]) let map_constr_expr_with_binders f g e = function @@ -490,12 +536,25 @@ let map_constr_expr_with_binders f g e = function | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x - | CCases (loc,po,a,bl) -> + | CCases (loc,(po,rtnpo),a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in - CCases (loc,option_app (f e) po,List.map (f e) a,bl) + let e' = + List.fold_right + (fun (tm,(na,indnal)) e -> + option_fold_right + (fun (loc,ind,nal) -> + List.fold_right (name_fold g) nal) indnal (name_fold g na e)) + a e + in + CCases (loc,(option_app (f e) po, option_app (f e') rtnpo), + List.map (fun (tm,x) -> (f e tm,x)) a,bl) | COrderedCase (loc,s,po,a,bl) -> COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl) + | CLetTuple (loc,nal,(na,po),b,c) -> + let e' = List.fold_right (name_fold g) nal e in + let e'' = name_fold g na e in + CLetTuple (loc,nal,(na,option_app (f e'') po),f e b,f e' c) | CFix (loc,id,dl) -> CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,f e t,f e d)) dl) | CCoFix (loc,id,dl) -> diff --git a/interp/topconstr.mli b/interp/topconstr.mli index f5f620528c..55cd20290f 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -29,9 +29,11 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ACases of aconstr option * aconstr list * + | ACases of aconstr option * aconstr option * + (aconstr * (name * (inductive * name list) option)) list * (identifier list * cases_pattern list * aconstr) list | AOrderedCase of case_style * aconstr option * aconstr * aconstr array + | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | ASort of rawsort | AHole of hole_kind | APatVar of patvar @@ -62,7 +64,7 @@ type notation = string type explicitation = int -type proj_flag = bool (* [true] = is projection *) +type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier @@ -82,10 +84,13 @@ type constr_expr = | 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 * + | CCases of loc * (constr_expr option * constr_expr option) * + (constr_expr * (name * (loc * reference * name list) option)) list * (loc * cases_pattern_expr list * constr_expr) list | COrderedCase of loc * case_style * constr_expr option * constr_expr * constr_expr list + | CLetTuple of loc * name list * (name * constr_expr option) * + constr_expr * constr_expr | CHole of loc | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key |