diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-11 10:25:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-11 10:25:04 +0000 |
| commit | ead31bf3e2fe220d02dec59dce66471cc2c66fce (patch) | |
| tree | f2dc8aa43dda43200654e8e28a7556f7b84ae200 | |
| parent | aad98c46631f3acb3c71ff7a7f6ae9887627baa8 (diff) | |
Nouvelle mouture du traducteur v7->v8
Option -v8 Ã coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
48 files changed, 1493 insertions, 604 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index 66ac7b97e..7394a41c5 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -180,7 +180,7 @@ let rawconstr_of_prog p = let (bl',avoid',nenv') = push_vars avoid nenv bl in let c1 = trad avoid nenv e1 and c2 = trad avoid' nenv' e2 in - ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |]) + ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None) | CC_lam (bl,e) -> let bl',avoid',nenv' = push_vars avoid nenv bl in @@ -214,7 +214,7 @@ let rawconstr_of_prog p = let c = trad avoid nenv b in let cl = List.map (trad avoid nenv) el in let ty = Detyping.detype (Global.env()) avoid nenv ty in - ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl) + ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None) | CC_expr c -> Detyping.detype (Global.env()) avoid nenv c diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 0e6b3b7d2..2e3fcac41 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -107,7 +107,7 @@ open Coqast let mk_id loc id = mkRefC (Ident (loc, id)) let mk_ref loc s = mk_id loc (id_of_string s) let mk_appl loc1 loc2 f args = - CApp (join_loc loc1 loc2, (false,mk_ref loc1 f), List.map (fun a -> a,None) args) + CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args) let conj_assert {a_name=n;a_value=a} {a_value=b} = let loc1 = constr_loc a in @@ -166,7 +166,7 @@ let rec coqast_of_program loc = function (function Term t -> (coqast_of_program t.loc t.desc,None) | _ -> invalid_arg "coqast_of_program") l in - CApp (dummy_loc, (false,f), args) + CApp (dummy_loc, (None,f), args) | Expression c -> bdize c | _ -> invalid_arg "coqast_of_program" diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 487f45057..3d01dd92f 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -144,7 +144,7 @@ let (imply_intro1: pbp_rule) = function let make_var id = CRef (Ident(zz, id)) -let make_app f l = CApp (zz,(false,f),List.map (fun x -> (x,None)) l) +let make_app f l = CApp (zz,(None,f),List.map (fun x -> (x,None)) l) let make_pbp_pattern x = make_app (make_var (id_of_string "PBP_META")) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c0ba10bdd..8d82da7e1 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -313,14 +313,17 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function xlate_formula_ne_list l) | CApp(_, (_,f), l) -> (* TODO: proj notation *) CT_appc(xlate_formula f, xlate_formula_expl_ne_list l) - | CCases (_,po,tml,eqns)-> CT_cases(xlate_formula_opt po, - xlate_formula_ne_list tml, + | CCases (_,(po,None),tml,eqns)-> CT_cases(xlate_formula_opt po, + xlate_formula_ne_list (List.map fst tml), CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns)) + | CCases (_,(po,Some _),tml,eqns)-> xlate_error "TODO" | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> CT_if(xlate_formula_opt po, xlate_formula c,xlate_formula b1,xlate_formula b2) + | CLetTuple (_,l, (na,po), c, b) -> xlate_error "LetTuple: TODO" + | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) -> CT_inductive_let(xlate_formula_opt po, xlate_id_opt_ne_list l, @@ -1500,7 +1503,7 @@ let xlate_vernac = | (*Record from tactics/Record.v *) VernacRecord - ((add_coercion, s), binders, CSort (_,c1), rec_constructor_or_none, field_list) -> + (_, (add_coercion, s), binders, CSort (_,c1), rec_constructor_or_none, field_list) -> let record_constructor = xlate_ident_opt rec_constructor_or_none in CT_record ((if add_coercion then CT_coercion_atm else diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 102754384..29f3c437c 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 e5cfd0190..008957e1b 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 17405769a..d1c32e998 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 f6f9fe60d..5287ce5a2 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 5b1d2813b..d2ef146bf 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 f5f620528..55cd20290 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 diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 397189271..60848fdfd 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -284,12 +284,17 @@ let subst_constr_expr a loc subs = | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a) | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x - | CCases (_,po,a,bl) -> + | CCases (_,(po,rtntypo),a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in - CCases (loc,option_app subst po,List.map subst a,bl) + CCases (loc,(option_app subst po,option_app subst rtntypo), + List.map (fun (tm,x) -> subst tm,x) a,bl) | COrderedCase (_,s,po,a,bl) -> COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl) + | CLetTuple (_,nal,(na,po),a,b) -> + let na = name_app (subst_id subs) na in + let nal = List.map (name_app (subst_id subs)) nal in + CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b) | CFix (_,id,dl) -> CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl) | CCoFix (_,id,dl) -> diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4 index 679d174c2..4d4000b23 100644 --- a/parsing/g_cases.ml4 +++ b/parsing/g_cases.ml4 @@ -55,13 +55,17 @@ GEXTEND Gram operconstr: LEVEL "1" [ [ "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of"; OPT "|"; eqs = ne_eqn_list; "end" -> - CCases (loc, Some p, lc, eqs) + let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in + CCases (loc, (Some p,None), lc, eqs) | "Cases"; lc = LIST1 constr; "of"; OPT "|"; eqs = ne_eqn_list; "end" -> - CCases (loc, None, lc, eqs) + let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in + CCases (loc, (None,None), lc, eqs) | "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of"; "end" -> - CCases (loc, Some p, lc, []) + let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in + CCases (loc, (Some p,None), lc, []) | "Cases"; lc = LIST1 constr; "of"; "end" -> - CCases (loc, None, lc, []) ] ] + let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in + CCases (loc, (None,None), lc, []) ] ] ; END; diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 43dc060a5..5904906b0 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -127,12 +127,12 @@ GEXTEND Gram operconstr: [ "10" RIGHTA [ "!"; f = global; args = LIST0 (operconstr LEVEL "9") -> - CAppExpl (loc, (false,f), args) + CAppExpl (loc, (None,f), args) (* | "!"; f = global; "with"; b = binding_list -> <:ast< (APPLISTWITH $f $b) >> *) - | f = operconstr; args = LIST1 constr91 -> CApp (loc, (false,f), args) ] + | f = operconstr; args = LIST1 constr91 -> CApp (loc, (None,f), args) ] | "9" RIGHTA [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ] | "8" RIGHTA @@ -196,7 +196,7 @@ GEXTEND Gram | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" -> (match lc1 with | CPatVar (loc2,(false,n)) -> - CApp (loc,(false,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl) + CApp (loc,(None,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl) | _ -> Util.error "Second-order pattern-matching expects a head metavariable") | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" -> @@ -208,7 +208,7 @@ GEXTEND Gram | s = sort -> CSort (loc, s) | v = global -> CRef v | n = bigint -> CNumeral (loc,n) - | "!"; f = global -> CAppExpl (loc,(false,f),[]) + | "!"; f = global -> CAppExpl (loc,(None,f),[]) | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> CDelimiters (loc,key,c) ] ] ; diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 16691158f..f8bb62a22 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -20,8 +20,9 @@ open Topconstr open Util let constr_kw = - [ "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; - "let"; "if"; "then"; "else"; "struct"; "Prop"; "Set"; "Type"; ".(" ] + [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; + "end"; "as"; "let"; "if"; "then"; "else"; "return"; + "Prop"; "Set"; "Type"; ".(" ] let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw let _ = Options.v7 := false @@ -56,6 +57,7 @@ let match_bind_of_pat loc (oid,ty) = l1@l2 let mk_match (loc,cil,rty,br) = +(* let (lc,pargs) = List.split cil in let pr = match rty with @@ -64,7 +66,8 @@ let mk_match (loc,cil,rty,br) = let idargs = (* TODO: not forget the list lengths for PP! *) List.flatten (List.map (match_bind_of_pat loc) pargs) in Some (CLambdaN(loc,idargs,ty)) in - CCases(loc,pr,lc,br) +*) + CCases(loc,(None,rty),cil,br) let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) = let n = @@ -101,9 +104,28 @@ let mk_fix(loc,kw,id,dcls) = let binder_constr = create_constr_entry (get_univ "constr") "binder_constr" + +let rec mkCProdN loc bll c = + match bll with + | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> + CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c) + | LocalRawDef ((loc1,_) as id,b) :: bll -> + CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c) + | [] -> c + | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c + +let rec mkCLambdaN loc bll c = + match bll with + | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> + CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c) + | LocalRawDef ((loc1,_) as id,b) :: bll -> + CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c) + | [] -> c + | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c + GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr sort global - constr_pattern Constr.ident; + constr_pattern Constr.ident binder_let tuple_constr; Constr.ident: [ [ id = Prim.ident -> id @@ -130,6 +152,12 @@ GEXTEND Gram constr: [ [ c = operconstr LEVEL "9" -> c ] ] ; + tuple_constr: + [ + [ (*c1 = tuple_constr; ","; c2 = tuple_constr -> + CNotation (loc,"_ , _",[c1;c2]) + | *) c = operconstr -> c ] ] + ; operconstr: [ "200" RIGHTA [ c = binder_constr -> c ] @@ -142,33 +170,39 @@ GEXTEND Gram | "40L" LEFTA [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ] | "10L" LEFTA - [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(false,f),args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(false,f),args) ] + [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args) + | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) + | c=operconstr; ".("; f=global; args1=LIST0 appl_arg; ")"; + args2=LIST0 appl_arg -> + CApp(loc,(Some (List.length args1+1),CRef f),args1@(c,None)::args2) + | c=operconstr; ".("; "@"; f=global; args1=LIST0 NEXT; ")"; + args2=LIST0 NEXT -> + CAppExpl(loc,(Some (List.length args1+1),f),args1@c::args2) ] | "9" [ ] | "1L" LEFTA - [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) - | c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> - CApp(loc,(true,CRef f),args@[c,None]) - | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT -> - CAppExpl(loc,(false,f),args@[c]) ] + [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ] | "0" [ c=atomic_constr -> c | c=match_constr -> c - | "("; c=operconstr; ")" -> c ] ] + | "("; c=tuple_constr; ")" -> c ] ] ; binder_constr: - [ [ "!"; bl = binder_list; "."; c = operconstr LEVEL "200" -> - CProdN(loc,bl,c) - | "fun"; bl = LIST1 binder; ty = type_cstr; "=>"; + [ [ "forall"; bl = binder_list; ","; c = operconstr LEVEL "200" -> + mkCProdN loc bl c + | "fun"; bl = binder_list; ty = type_cstr; "=>"; c = operconstr LEVEL "200" -> - CLambdaN(loc,bl,mk_cast(c,ty)) - | "let"; id=name; bl = LIST0 binder; ty = type_cstr; ":="; - c1 = operconstr; "in"; c2 = operconstr LEVEL "200" -> - CLetIn(loc,id,mk_lam(bl,mk_cast(c1,ty)),c2) - | "let"; "("; lb = LIST1 name SEP ","; ")"; ":="; + mkCLambdaN loc bl (mk_cast(c,ty)) + | "let"; id=name; bl = LIST0 binder_let; ty = type_cstr; ":="; c1 = operconstr; "in"; c2 = operconstr LEVEL "200" -> - COrderedCase (loc, LetStyle, None, c1, - [CLambdaN (loc, [lb, CHole loc], c2)]) + let loc1 = match bl with + | LocalRawAssum ((loc,_)::_,_)::_ -> loc + | LocalRawDef ((loc,_),_)::_ -> loc + | _ -> dummy_loc in + CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) + | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; + po = return_type; + ":="; c1 = operconstr; "in"; c2 = operconstr LEVEL "200" -> + CLetTuple (loc,List.map snd lb,po,c1,c2) | "if"; c1=operconstr; "then"; c2=operconstr LEVEL "200"; "else"; c3=operconstr LEVEL "200" -> COrderedCase (loc, IfStyle, None, c1, [c2; c3]) @@ -205,7 +239,7 @@ GEXTEND Gram c=operconstr LEVEL "200" -> (loc,id,bl,ann,c,ty) ] ] ; fixannot: - [ [ "{"; "struct"; id=name; "}" -> Some id + [ [ "{"; IDENT "struct"; id=name; "}" -> Some id | -> None ] ] ; match_constr: @@ -213,14 +247,23 @@ GEXTEND Gram br=branches; "end" -> mk_match (loc,ci,ty,br) ] ] ; case_item: - [ [ c=operconstr LEVEL "80"; p=pred_pattern -> (c,p) ] ] + [ [ c=operconstr LEVEL "100"; p=pred_pattern -> + match c,p with + | CRef (Ident (_,id)), (Names.Anonymous,x) -> (c,(Name id,x)) + | _ -> (c,p) ] ] ; pred_pattern: - [ [ oid = OPT ["as"; id=name -> id]; - (_,ty) = type_cstr -> (oid,ty) ] ] + [ [ oid = ["as"; id=name -> snd id | -> Names.Anonymous]; + ty = OPT ["in"; r=global; nal=LIST0 name -> + (loc,r,List.map snd nal)] -> + (oid,ty) ] ] ; case_type: - [ [ ty = OPT [ "=>"; c = lconstr -> c ] -> ty ] ] + [ [ ty = OPT [ "return"; c = operconstr LEVEL "100" -> c ] -> ty ] ] + ; + return_type: + [ [ na = ["as"; id=name -> snd id | -> Names.Anonymous]; + ty = case_type -> (na,ty) ] ] ; branches: [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] @@ -252,9 +295,25 @@ GEXTEND Gram | p1=pattern; ","; p2=lpattern -> CPatCstr (loc, pair loc, [p1;p2]) ] ] ; binder_list: - [ [ idl=LIST1 name; bl=LIST0 binder -> (idl,CHole loc)::bl - | "("; idl=LIST1 name; ":"; c=lconstr; ")"; bl=LIST0 binder ->(idl,c)::bl - | idl=LIST1 name; ":"; c=constr -> [(idl,c)] ] ] + [ [ idl=LIST1 name; bl=LIST0 binder_let -> + LocalRawAssum (idl,CHole loc)::bl + | idl=LIST1 name; ":"; c=lconstr -> + [LocalRawAssum (idl,c)] + | "("; idl=LIST1 name; ":"; c=lconstr; ")"; bl=LIST0 binder_let -> + LocalRawAssum (idl,c)::bl ] ] + ; + binder_let: + [ [ id=name -> + LocalRawAssum ([id],CHole loc) + | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> + LocalRawAssum (id::idl,c) + | "("; id=name; ":"; c=lconstr; ")" -> + LocalRawAssum ([id],c) + | "("; id=name; ":="; c=lconstr; ")" -> + LocalRawDef (id,c) + | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> + LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,t)) + ] ] ; binder: [ [ id=name -> ([id],CHole loc) diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 986e6b058..ad78104cf 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -73,8 +73,8 @@ GEXTEND Gram tactic_expr: [ "5" LEFTA - [ ta0 = tactic_expr; "&"; ta1 = tactic_expr -> TacThen (ta0, ta1) - | ta = tactic_expr; "&"; "["; lta = LIST0 tactic_expr SEP "|"; "]" -> + [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1) + | ta = tactic_expr; ";"; "["; lta = LIST0 tactic_expr SEP "|"; "]" -> TacThens (ta, lta) ] | "4" [ ] @@ -186,10 +186,12 @@ GEXTEND Gram ; (* Definitions for tactics *) +(* deftok: [ [ IDENT "Meta" | IDENT "Tactic" ] ] ; +*) tacdef_body: [ [ name = identref; it=LIST1 input_fun; ":="; body = tactic_expr -> (name, TacFun (it, body)) @@ -200,9 +202,7 @@ GEXTEND Gram [ [ tac = tactic_expr -> tac ] ] ; Vernac_.command: - [ [ deftok; "Definition"; b = tacdef_body -> - VernacDeclareTacticDefinition (false, [b]) - | IDENT "Recursive"; deftok; "Definition"; + [ [ IDENT "Ltac"; l = LIST1 tacdef_body SEP "with" -> VernacDeclareTacticDefinition (true, l) ] ] ; diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4 index de18ab764..4ca29e232 100644 --- a/parsing/g_primnew.ml4 +++ b/parsing/g_primnew.ml4 @@ -22,7 +22,7 @@ let _ = f Prim.ast; f Prim.reference -let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'";"."] +let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'"] let _ = List.iter (fun s -> Lexer.add_token("",s)) prim_kw ifdef Quotify then @@ -83,7 +83,7 @@ GEXTEND Gram [ [ s = METAIDENT -> Nmeta (loc,s) ] ] ; field: - [ [ "."; s = IDENT -> local_id_of_string s ] ] + [ [ s = FIELD -> local_id_of_string s ] ] ; fields: [ [ id = field; (l,id') = fields -> (local_append l id,id') diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 5b2e165ac..0c9e0ce26 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -124,11 +124,11 @@ GEXTEND Gram [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, HintsResolve - (List.map (fun qid -> (None, CAppExpl(loc,(false,qid),[]))) l)) + (List.map (fun qid -> (None, CAppExpl(loc,(None,qid),[]))) l)) | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, HintsImmediate - (List.map (fun qid-> (None, CAppExpl (loc,(false,qid),[]))) l)) + (List.map (fun qid-> (None, CAppExpl (loc,(None,qid),[]))) l)) | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ] ; diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4 index 82896099f..e0e374426 100644 --- a/parsing/g_proofsnew.ml4 +++ b/parsing/g_proofsnew.ml4 @@ -61,9 +61,8 @@ GEXTEND Gram | IDENT "Unfocus" -> VernacUnfocus | IDENT "Show" -> VernacShow (ShowGoal None) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n)) - | IDENT "Show"; IDENT "Implicits"; n = natural -> - VernacShow (ShowGoalImplicitly (Some n)) - | IDENT "Show"; IDENT "Implicits" -> VernacShow (ShowGoalImplicitly None) + | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural -> + VernacShow (ShowGoalImplicitly n) | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index bd71bbd5c..017cfd18f 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -135,7 +135,7 @@ GEXTEND Gram (Some (nl,c1), c2) ] ] ; pattern_occ: - [ [ nl = LIST0 integer; c = [c=constr->c | g=global->Topconstr.CRef g]-> (nl,c) ] ] + [ [ c = constr; nl = LIST0 integer -> (nl,c) ] ] ; pattern_occ_hyp_tail_list: [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ] @@ -176,7 +176,7 @@ GEXTEND Gram [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ] ; unfold_occ: - [ [ nl = LIST0 integer; c = global -> (nl,c) ] ] + [ [ c = global; nl = LIST0 integer -> (nl,c) ] ] ; red_flag: [ [ IDENT "beta" -> FBeta @@ -194,9 +194,9 @@ GEXTEND Gram | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s) | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s) | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta]) - | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul + | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl - | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl ] ] + | IDENT "pattern"; pl = LIST1 pattern_occ SEP "," -> Pattern pl ] ] ; (* This is [red_tactic] including possible extensions *) red_expr: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0d431ea93..d038e7d8c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -183,8 +183,8 @@ GEXTEND Gram ; gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = base_ident; bl = binders_list; ":"; c = constr -> - VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ())) + [ [ thm = thm_token; id = base_ident; ":"; c = constr -> + VernacStartTheoremProof (thm, id, ([], c), false, (fun _ _ -> ())) | (f,d,e) = def_token; id = base_ident; b = def_body -> VernacDefinition (d, id, b, f, e) | stre = assumption_token; bl = ne_params_list -> @@ -200,7 +200,7 @@ GEXTEND Gram | "CoInductive" -> false ] ] ; record_token: - [ [ IDENT "Record" -> () | IDENT "Structure" -> () ] ] + [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ] ; constructor: [ [ idl = LIST1 base_ident SEP ","; coe = of_type_with_opt_coercion; @@ -305,10 +305,10 @@ GEXTEND Gram indl = block_old_style -> let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in VernacInductive (f,indl') - | record_token; oc = opt_coercion; name = base_ident; + | b = record_token; oc = opt_coercion; name = base_ident; ps = simple_binders_list; ":"; s = constr; ":="; c = rec_constructor; "{"; fs = fields; "}" -> - VernacRecord ((oc,name),ps,s,c,fs) + VernacRecord (b,(oc,name),ps,s,c,fs) ] ] ; gallina: @@ -422,7 +422,7 @@ GEXTEND Gram let c = match n with | Some n -> let l = list_tabulate (fun _ -> (CHole (loc),None)) n in - CApp (loc,(false,c),l) + CApp (loc,(None,c),l) | None -> c in VernacNotation (false,c,Some("'"^id^"'",[]),None,None) | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 809ba58cf..a9866b7e8 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -42,13 +42,13 @@ let def_body = Gram.Entry.create "vernac:def_body" GEXTEND Gram GLOBAL: vernac gallina_ext; vernac: - (* Better to parse ";" here: in case of failure (e.g. in coerce_to_var), *) - (* ";" is still in the stream and discard_to_dot works correctly *) - [ [ g = gallina; ";" -> g - | g = gallina_ext; ";" -> g - | c = command; ";" -> c - | c = syntax; ";" -> c - | "["; l = LIST1 located_vernac; "]"; ";" -> VernacList l + (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) + (* "." is still in the stream and discard_to_dot works correctly *) + [ [ g = gallina; "." -> g + | g = gallina_ext; "." -> g + | c = command; "." -> c + | c = syntax; "." -> c + | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l ] ] ; vernac: FIRST @@ -56,7 +56,7 @@ GEXTEND Gram ; vernac: LAST [ [ gln = OPT[n=natural; ":" -> n]; - tac = subgoal_command; ";" -> tac gln ] ] + tac = subgoal_command; "." -> tac gln ] ] ; subgoal_command: [ [ c = check_command -> c @@ -86,22 +86,27 @@ let no_coercion loc (c,x) = (loc,"no_coercion",Pp.str"no coercion allowed here"); x +let flatten_assum l = + List.flatten + (List.map (fun (oc,(idl,t)) -> List.map (fun id -> (oc,(id,t))) idl) l) + (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body; gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = base_ident; bl = LIST0 binder; ":"; + [ [ thm = thm_token; id = base_ident; (* bl = LIST0 binder; *) ":"; c = lconstr -> + let bl = [] in VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ())) | (f,d,e) = def_token; id = base_ident; b = def_body -> VernacDefinition (d, id, b, f, e) - | stre = assumption_token; bl = LIST1 simple_binder_coe -> - VernacAssumption (stre, bl) - | stre = assumptions_token; bl = LIST1 simple_binder_coe -> + | stre = assumption_token; bl = LIST1 assum_coe -> + VernacAssumption (stre, flatten_assum bl) + | stre = assumptions_token; bl = LIST1 assum_coe -> test_plurial_form bl; - VernacAssumption (stre, bl) + VernacAssumption (stre, flatten_assum bl) (* Gallina inductive declarations *) | (* Non porté (?) : OPT[IDENT "Mutual"];*) f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -113,11 +118,11 @@ GEXTEND Gram | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ] ; gallina_ext: - [ [ record_token; oc = opt_coercion; name = base_ident; + [ [ b = record_token; oc = opt_coercion; name = base_ident; ps = LIST0 simple_binder; ":"; s = lconstr; ":="; cstr = OPT base_ident; "{"; - fs = LIST0 local_decl_expr; "}" -> - VernacRecord ((oc,name),ps,s,cstr,fs) + fs = LIST0 record_field SEP ";"; "}" -> + VernacRecord (b,(oc,name),ps,s,cstr,fs) (* Non porté ? | f = finite_token; s = csort; id = base_ident; indpar = LIST0 simple_binder; ":="; lc = constructor_list -> @@ -154,17 +159,17 @@ GEXTEND Gram | "CoInductive" -> false ] ] ; record_token: - [ [ IDENT "Record" -> () | IDENT "Structure" -> () ] ] + [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ] ; (* Simple definitions *) def_body: - [ [ bl = LIST0 binder; ":="; red = reduce; c = lconstr -> + [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr -> (match c with CCast(_,c,t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) - | bl = LIST0 binder; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> + | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) - | bl = LIST0 binder; ":"; t = lconstr -> + | bl = LIST0 binder_let; ":"; t = lconstr -> ProveBody (bl, t) ] ] ; reduce: @@ -182,8 +187,8 @@ GEXTEND Gram (id,ntn,indpar,c,lc) ] ] ; constructor_list: - [ [ "|"; l = LIST1 constructor_binder SEP "|" -> l - | l = LIST1 constructor_binder SEP "|" -> l + [ [ "|"; l = LIST1 constructor SEP "|" -> l + | l = LIST1 constructor SEP "|" -> l | -> [] ] ] ; (* @@ -225,7 +230,7 @@ GEXTEND Gram (id,CProdN(loc,bl,c),CLambdaN(loc,bl,def)) ] ] ; rec_annotation: - [ [ "{"; "struct"; id=IDENT; "}" -> id_of_string id ] ] + [ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ] ; type_cstr: [ [ ":"; c=lconstr -> c @@ -246,17 +251,8 @@ GEXTEND Gram simple_binder: [ [ b = simple_binder_coe -> no_coercion loc b ] ] ; - binder: - [ [ na = name -> LocalRawAssum([na],CHole loc) - | "("; na = name; ")" -> LocalRawAssum([na],CHole loc) - | "("; na = name; ":"; c = lconstr; ")" - -> LocalRawAssum([na],c) - | "("; na = name; ":="; c = lconstr; ")" -> - LocalRawDef (na,c) - ] ] - ; binder_nodef: - [ [ b = binder -> + [ [ b = binder_let -> (match b with LocalRawAssum(l,ty) -> (l,ty) | LocalRawDef _ -> @@ -264,20 +260,21 @@ GEXTEND Gram (loc,"fix_param",Pp.str"defined binder not allowed here")) ] ] ; (* ... with coercions *) - local_decl_expr: + record_field: [ [ id = base_ident -> (false,AssumExpr(id,CHole loc)) - | "("; id = base_ident; ")" -> (false,AssumExpr(id,CHole loc)) - | "("; id = base_ident; oc = of_type_with_opt_coercion; - t = lconstr; ")" -> + | id = base_ident; oc = of_type_with_opt_coercion; t = lconstr -> (oc,AssumExpr (id,t)) - | "("; id = base_ident; oc = of_type_with_opt_coercion; - t = lconstr; ":="; b = lconstr; ")" -> - (oc,DefExpr (id,b,Some t)) - | "("; id = base_ident; ":="; b = lconstr; ")" -> + | id = base_ident; oc = of_type_with_opt_coercion; + t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t)) + | id = base_ident; ":="; b = lconstr -> match b with CCast(_,b,t) -> (false,DefExpr(id,b,Some t)) | _ -> (false,DefExpr(id,b,None)) ] ] ; + assum_coe: + [ [ "("; idl = LIST1 base_ident; oc = of_type_with_opt_coercion; + c = lconstr; ")" -> (oc,(idl,c)) ] ] + ; simple_binder_coe: [ [ id=base_ident -> (false,(id,CHole loc)) | "("; id = base_ident; ")" -> (false,(id,CHole loc)) @@ -285,7 +282,7 @@ GEXTEND Gram t = lconstr; ")" -> (oc,(id,t)) ] ] ; - constructor_binder: + constructor: [ [ id = base_ident; coe = of_type_with_opt_coercion; c = lconstr -> (coe,(id,c)) ] ] ; @@ -431,8 +428,10 @@ GEXTEND Gram | None -> c in VernacNotation (false,c,Some("'"^id^"'",[]),None,None) *) - | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> - VernacDeclareImplicits (qid,Some l) + | IDENT "Implicit"; IDENT "Arguments"; qid = global; + pos = OPT [ "["; l = LIST0 natural; "]" -> l ] -> + VernacDeclareImplicits (qid,pos) + | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None) | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"]; @@ -598,8 +597,8 @@ GEXTEND Gram | IDENT "Scope"; s = IDENT -> PrintScope s ] ] ; class_rawexpr: - [ [ IDENT "FUNCLASS" -> FunClass - | IDENT "SORTCLASS" -> SortClass + [ [ IDENT "Funclass" -> FunClass + | IDENT "Sortclass" -> SortClass | qid = global -> RefClass qid ] ] ; locatable: @@ -669,11 +668,11 @@ GEXTEND Gram | IDENT "Arguments"; IDENT "Scope"; qid = global; "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) - | IDENT "Infix"; local = locality; a = entry_prec; n = OPT natural; + | IDENT "Infix"; local = locality; (*a = entry_prec; n = OPT natural; *) op = STRING; p = global; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - let (a,n,b) = Metasyntax.interp_infix_modifiers a n modl in + let (a,n,b) = Metasyntax.interp_infix_modifiers None None modl in VernacInfix (local,a,n,op,p,b,None,sc) | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr; l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing] diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5e27f9ca8..5545f0077 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -309,7 +309,7 @@ let parse_226_tail tk = parser (* Parse what follows a dot *) let parse_after_dot bp c strm = - if !Options.v7 then + if (* !Options.v7 *) true then match strm with parser | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] -> ("FIELD", get_buff len) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 39047e688..476b3abd5 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -353,6 +353,8 @@ module Constr = let pattern = Gram.Entry.create "constr:pattern" let annot = Gram.Entry.create "constr:annot" let constr_pattern = gec_constr "constr_pattern" + let binder_let = Gram.Entry.create "constr:binder_list" + let tuple_constr = Gram.Entry.create "constr:tuple_constr" end module Module = @@ -618,6 +620,11 @@ let get_constr_entry en = snd (get_entry (get_univ "constr") "binder_constr"), None, false + | ETConstr(250,()) when not !Options.v7 -> + weaken_entry Constr.tuple_constr, +(* snd (get_entry (get_univ "constr") "tuple_construple"),*) + None, + false | _ -> compute_entry true (fun (n,()) -> Some n) en (* This computes the name to give to a production knowing the name and diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7bf1d837d..a591f57b2 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -138,6 +138,8 @@ module Constr : val pattern : cases_pattern_expr Gram.Entry.e val annot : constr_expr Gram.Entry.e val constr_pattern : constr_expr Gram.Entry.e + val binder_let : local_binder Gram.Entry.e + val tuple_constr : constr_expr Gram.Entry.e end module Module : diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 361e24647..b3118f7e7 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -203,13 +203,13 @@ let pr_eqn pr (_,patl,rhs) = str "=>" ++ brk (1,1) ++ pr ltop rhs) ++ spc () -let pr_cases pr po tml eqns = +let pr_cases pr (po,_) tml eqns = hov 0 ( pr_annotation pr po ++ hv 0 ( hv 0 ( str "Cases" ++ brk (1,2) ++ - prlist_with_sep spc (pr ltop) tml ++ spc() ++ str "of") ++ brk(1,2) ++ + prlist_with_sep spc (fun (tm,_) -> pr ltop tm) tml ++ spc() ++ str "of") ++ brk(1,2) ++ prlist_with_sep (fun () -> str "| ") (pr_eqn pr) eqns ++ str "end")) @@ -247,15 +247,10 @@ let rec pr inherited a = hv 1 ( hv 1 (str "[" ++ pr_let_binder pr (snd x) a ++ bll ++ str "]") ++ brk (0,1) ++ b), lletin - | CAppExpl (_,(true,f),l) -> - let a,l = list_sep_last l in - pr_proj pr pr_explapp a f l, lapp - | CAppExpl (_,(false,f),l) -> pr_explapp pr f l, lapp - | CApp (_,(true,a),l) -> - let c,l = list_sep_last l in - assert (snd c = None); - pr_proj pr pr_app (fst c) a l, lapp - | CApp (_,(false,a),l) -> pr_app pr a l, lapp + | CAppExpl (_,((* V7 don't know about projections *)_,f),l) -> + pr_explapp pr f l, lapp + | CApp (_,(_,a),l) -> + pr_app pr a l, lapp | CCases (_,po,tml,eqns) -> pr_cases pr po tml eqns, lcases | COrderedCase (_,IfStyle,po,c,[b1;b2]) -> @@ -267,15 +262,9 @@ let rec pr inherited a = str "if " ++ pr ltop c ++ spc () ++ hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++ hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif - | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,CHole _ as bd],b)]) -> - hov 0 ( - pr_annotation pr po ++ - hv 0 ( - str "let" ++ brk (1,1) ++ - hov 0 (str "(" ++ pr_binder pr bd ++ str ")") ++ - str " =" ++ brk (1,2) ++ - pr ltop c ++ spc () ++ - str "in " ++ pr ltop b)), lletin + | CLetTuple (_,nal,(na,po),c,b) -> + error "Let tuple not supported in v7" + | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) -> hov 0 ( hov 0 ( diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 697c78890..9326ff538 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -194,8 +194,8 @@ let rec mlexpr_of_constr = function | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> - | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >> + | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> + | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >> | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >> diff --git a/parsing/termast.ml b/parsing/termast.ml index 9f09c14be..9cc66a37f 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -222,14 +222,15 @@ let rec ast_of_raw = function (* Pour compatibilité des theories, il faut LAMBDALIST partout *) ope("LAMBDALIST",[ast_of_raw t;a]) - | RCases (_,typopt,tml,eqns) -> + | RCases (_,(typopt,_),tml,eqns) -> let pred = ast_of_rawopt typopt in let tag = "CASES" in - let asttomatch = ope("TOMATCH", List.map ast_of_raw tml) in + let asttomatch = + ope("TOMATCH", List.map (fun (tm,_) -> ast_of_raw tm) tml) in let asteqns = List.map ast_of_eqn eqns in ope(tag,pred::asttomatch::asteqns) - | ROrderedCase (_,LetStyle,typopt,tm,[|bv|]) -> + | ROrderedCase (_,LetStyle,typopt,tm,[|bv|],_) -> let nvar' = function Anonymous -> nvar wildcard | Name id -> nvar id in let rec f l = function | RLambda (_,na,RHole _,c) -> f (nvar' na :: l) c @@ -239,7 +240,7 @@ let rec ast_of_raw = function let eqn = ope ("EQN", [c;ope ("PATTCONSTRUCT",(nvar wildcard)::l)]) in ope ("FORCELET",[(ast_of_rawopt typopt);(ast_of_raw tm);eqn]) - | ROrderedCase (_,st,typopt,tm,bv) -> + | ROrderedCase (_,st,typopt,tm,bv,_) -> let tag = match st with | IfStyle -> "FORCEIF" | RegularStyle -> "CASE" @@ -250,6 +251,10 @@ let rec ast_of_raw = function ope(tag,(ast_of_rawopt typopt) ::(ast_of_raw tm) ::(Array.to_list (Array.map ast_of_raw bv))) + + | RLetTuple (loc,nal,(na,typopt),tm,b) -> + error "Let tuple not supported in v7" + | RRec (_,fk,idv,tyv,bv) -> let alfi = Array.map ast_of_ident idv in (match fk with diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c24748970..e2aa74cba 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -591,11 +591,15 @@ let occur_rawconstr id = | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c)) - | RCases (loc,tyopt,tml,pl) -> - (occur_option tyopt) or (List.exists occur tml) + | RCases (loc,(tyopt,rtntypopt),tml,pl) -> + (occur_option tyopt) or (occur_option !rtntypopt) + or (List.exists (fun (tm,_) -> occur tm) tml) or (List.exists occur_pattern pl) - | ROrderedCase (loc,b,tyopt,tm,bv) -> + | ROrderedCase (loc,b,tyopt,tm,bv,_) -> (occur_option tyopt) or (occur tm) or (array_exists occur bv) + | RLetTuple (loc,nal,(na,tyopt),b,c) -> + (na <> Name id & occur_option tyopt) + or (occur b) or (not (List.mem (Name id) nal) & (occur c)) | RRec (loc,fk,idl,tyl,bv) -> (array_exists occur tyl) or (not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv) @@ -1546,6 +1550,45 @@ let extract_predicate_conclusion nargs pred = | _ -> (* eta-expansion *) applist (lift 1 p, [mkRel 1]) in iterate decomp_lam_force nargs pred +let set_arity_signature dep n arsign tomatchl pred x = + (* avoid is not exhaustive ! *) + let rec decomp_lam_force n avoid l p = + if n = 0 then (List.rev l,p,avoid) else + match p with + | RLambda (_,(Name id as na),_,c) -> + decomp_lam_force (n-1) (id::avoid) (na::l) c + | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c + | _ -> + let x = next_ident_away (id_of_string "x") avoid in + decomp_lam_force (n-1) (x::avoid) (Name x :: l) + (* eta-expansion *) + (let a = RVar (dummy_loc,x) in + match p with + | RApp (loc,p,l) -> RApp (loc,p,l@[a]) + | _ -> (RApp (dummy_loc,p,[a]))) in + let rec decomp_block avoid p = function + | ([], _) -> x := Some p + | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l') -> + let (ind,params) = dest_ind_family indf in + let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p + in + let na,p,avoid' = + if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid' + in + y := + (List.hd na, + if List.for_all ((=) Anonymous) nal then + None + else + Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal)); + decomp_block avoid' p (l,l') + | (_::l),(y::l') -> + y := (Anonymous,None); + decomp_block avoid p (l,l') + | _ -> anomaly "set_arity_signature" + in + decomp_block [] pred (tomatchl,arsign) + let prepare_predicate_from_tycon loc dep env isevars tomatchs c = let cook (n, l, env) = function | c,IsInd (_,IndType(indf,realargs)) -> @@ -1571,7 +1614,7 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c = map_constr_with_full_binders push_rel build_skeleton env c in build_skeleton env (lift n c) -(* Here, [pred] is assumed to be in the context build from all *) +(* Here, [pred] is assumed to be in the context built from all *) (* realargs and terms to match *) let build_initial_predicate env sigma isdep pred tomatchl = let cook n = function @@ -1595,6 +1638,45 @@ let build_initial_predicate env sigma isdep pred tomatchl = PrLetIn ((realargs,None), buildrec (n+nrealargs) q ltm) in buildrec 0 0 tomatchl +let extract_arity_signature env0 tomatchl tmsign = + let get_one_sign n tm {contents = (na,t)} = + match tm with + | NotInd _ -> + (match t with + | None -> [] + | Some (loc,_,_) -> + user_err_loc (loc,"", + str "Unexpected type annotation for a term of non inductive type")) + | IsInd (_,IndType(indf,realargs)) -> + let indf' = lift_inductive_family n indf in + let (ind,params) = dest_ind_family indf' in + let nrealargs = List.length realargs in + let realnal = + match t with + | Some (loc,ind',nal) -> + let nparams = List.length params in + if ind <> ind' then + user_err_loc (loc,"",str "Wrong inductive type"); + if List.length nal <> nparams + nrealargs then + user_err_loc (loc,"", + str "Wrong number of arguments for inductive type"); + let parnal,realnal = list_chop nparams nal in + if List.exists ((<>) Anonymous) parnal then + user_err_loc (loc,"", + str "The parameters of inductive type must be implicit"); + List.rev realnal + | None -> list_tabulate (fun _ -> Anonymous) nrealargs in + let arsign = fst (get_arity env0 indf') in + (na,None,build_dependent_inductive env0 indf') + ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in + let rec buildrec n = function + | [],[] -> [] + | (_,tm)::ltm, x::tmsign -> + let l = get_one_sign n tm x in + (buildrec (n + List.length l) (ltm,tmsign)) @ l + | _ -> assert false + in buildrec 0 (tomatchl,tmsign) + (* determines wether the multiple case is dependent or not. For that * the predicate given by the user is eta-expanded. If the result * of expansion is pred, then : @@ -1606,15 +1688,28 @@ let build_initial_predicate env sigma isdep pred tomatchl = * else error! (can not treat mixed dependent and non dependent case *) -let prepare_predicate loc typing_fun isevars env tomatchs tycon = function - | None -> +let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function + (* No type annotation at all *) + | (None,{contents = None}) -> (match tycon with | None -> None | Some t -> let pred = prepare_predicate_from_tycon loc false env isevars tomatchs t in Some (build_initial_predicate env (evars_of isevars) false pred tomatchs)) - | Some pred -> + + (* v8 style type annotation *) + | (None,{contents = Some rtntyp}) -> + + (* We extract the signature of the arity *) + let arsign = extract_arity_signature env tomatchs sign in + let env = push_rels arsign env in + let predccl = (typing_fun empty_tycon env rtntyp).uj_val in + Some + (build_initial_predicate env (evars_of isevars) true predccl tomatchs) + + (* v7 style type annotation; set the v8 annotation by side effect *) + | (Some pred,x) -> let loc = loc_of_rawconstr pred in let dep, n, predj = let isevars_copy = evars_of isevars in @@ -1643,6 +1738,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs tycon = function (* let etapred,cdep = case_dependent env (evars_of isevars) loc predj tomatchs in *) + set_arity_signature dep n sign tomatchs pred x; Some(build_initial_predicate env (evars_of isevars) dep predccl tomatchs) @@ -1656,11 +1752,12 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)= (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) - let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in + let rawtms, tmsign = List.split tomatchl in + let tomatchs = coerce_to_indtype typing_fun isevars env matx rawtms in (* We build the elimination predicate if any and check its consistency *) (* with the type of arguments to match *) - let pred = prepare_predicate loc typing_fun isevars env tomatchs tycon predopt in + let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in (* We deal with initial aliases *) let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 287e78f76..1c4e6b92c 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -41,6 +41,8 @@ type ml_case_error = exception NotInferable of ml_case_error +val occur_rawconstr : identifier -> rawconstr -> bool + val pred_case_ml : (* raises [NotInferable] if not inferable *) env -> evar_map -> bool -> inductive_type -> int * types -> constr @@ -49,6 +51,7 @@ val pred_case_ml : (* raises [NotInferable] if not inferable *) val compile_cases : loc -> (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs -> type_constraint -> env -> - rawconstr option * rawconstr list * + (rawconstr option * rawconstr option ref) * + (rawconstr * (name * (loc * inductive * name list) option) ref) list * (loc * identifier list * cases_pattern list * rawconstr) list -> unsafe_judgment diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 9e4eaf8a1..a82b2b90a 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -162,7 +162,6 @@ let computable p k = noccur_between 1 (k+1) ccl - let lookup_name_as_renamed env t s = let rec lookup avoid env_names n c = match kind_of_term c with | Prod (name,_,c') -> @@ -195,7 +194,7 @@ let lookup_index_as_renamed env t n = | _ -> None in lookup n 1 t -let detype_case computable detype detype_eqn tenv avoid env indsp st p c bl = +let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl = let synth_type = synthetize_type () in let tomatch = detype tenv avoid env c in @@ -207,11 +206,41 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p c bl = List.rev (fst (decompose_prod_assum t)) in let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in let consnargsl = Array.map List.length consnargs in - let pred = + let alias, aliastyp, newpred, pred = if synth_type & computable & bl <> [||] then - None - else - option_app (detype tenv avoid env) p in + Anonymous, None, None, None + else + let p = option_app (detype tenv avoid env) p in + match p with + | None -> Anonymous, None, None, None + | Some p -> + let decompose_lam k c = + let name_cons = function + Anonymous -> fun l -> l | Name id -> fun l -> id::l in + let rec lamdec_rec l avoid k c = + if k = 0 then l,c else match c with + | RLambda (_,x,t,c) -> + lamdec_rec (x::l) (name_cons x avoid) (k-1) c + | c -> + let x = next_ident_away (id_of_string "xx") avoid in + lamdec_rec ((Name x)::l) (x::avoid) (k-1) + (let a = RVar (dummy_loc,x) in + match c with + | RApp (loc,p,l) -> RApp (loc,p,l@[a]) + | _ -> (RApp (dummy_loc,c,[a]))) + in + lamdec_rec [] [] k c in + let nl,typ = decompose_lam k p in + let n,typ = match typ with + | RLambda (_,x,t,c) -> x, c + | _ -> Anonymous, typ in + let aliastyp = + if List.for_all ((=) Anonymous) nl then None + else + let pars = list_tabulate (fun _ -> Anonymous) mip.mind_nparams + in Some (dummy_loc,indsp,pars@nl) in + n, aliastyp, Some typ, Some p + in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in let eqnv = array_map3 (detype_eqn tenv avoid env) constructs consnargsl bl in let eqnl = Array.to_list eqnv in @@ -226,29 +255,48 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p c bl = with Not_found -> st in if tag = RegularStyle then - RCases (dummy_loc,pred,[tomatch],eqnl) + RCases (dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl) else - let rec remove_type avoid args c = - match c,args with - | RLambda (loc,na,t,c), _::args -> - let h = RHole (loc,BinderType na) in - RLambda (loc,na,h,remove_type avoid args c) - | RLetIn (loc,na,b,c), _::args -> - RLetIn (loc,na,b,remove_type avoid args c) - | c, (na,None,t)::args -> - let id = next_name_away_with_default "x" na avoid in - let h = RHole (dummy_loc,BinderType na) in - let c = remove_type (id::avoid) args - (RApp (dummy_loc,c,[RVar (dummy_loc,id)])) in - RLambda (dummy_loc,Name id,h,c) - | c, (na,Some b,t)::args -> - let h = RHole (dummy_loc,BinderType na) in - let avoid = name_fold (fun x l -> x::l) na avoid in - RLetIn (dummy_loc,na,h,remove_type avoid args c) - | c, [] -> c in let bl = Array.map (detype tenv avoid env) bl in - let bl = array_map2 (remove_type avoid) consnargs bl in - ROrderedCase (dummy_loc,tag,pred,tomatch,bl) + if not !Options.v7 && tag = LetStyle && aliastyp = None then + let rec decomp_lam_force n avoid l p = + if n = 0 then (List.rev l,p) else + match p with + | RLambda (_,(Name id as na),_,c) -> + decomp_lam_force (n-1) (id::avoid) (na::l) c + | RLambda (_,(Anonymous as na),_,c) -> + decomp_lam_force (n-1) avoid (na::l) c + | _ -> + let x = Nameops.next_ident_away (id_of_string "x") avoid in + decomp_lam_force (n-1) (x::avoid) (Name x :: l) + (* eta-expansion *) + (let a = RVar (dummy_loc,x) in + match p with + | RApp (loc,p,l) -> RApp (loc,p,l@[a]) + | _ -> (RApp (dummy_loc,p,[a]))) in + let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl.(0) in + RLetTuple (dummy_loc,nal,(alias,newpred),tomatch,d) + else + let rec remove_type avoid args c = + match c,args with + | RLambda (loc,na,t,c), _::args -> + let h = RHole (dummy_loc,BinderType na) in + RLambda (loc,na,h,remove_type avoid args c) + | RLetIn (loc,na,b,c), _::args -> + RLetIn (loc,na,b,remove_type avoid args c) + | c, (na,None,t)::args -> + let id = next_name_away_with_default "x" na avoid in + let h = RHole (dummy_loc,BinderType na) in + let c = remove_type (id::avoid) args + (RApp (dummy_loc,c,[RVar (dummy_loc,id)])) in + RLambda (dummy_loc,Name id,h,c) + | c, (na,Some b,t)::args -> + let h = RHole (dummy_loc,BinderType na) in + let avoid = name_fold (fun x l -> x::l) na avoid in + RLetIn (dummy_loc,na,h,remove_type avoid args c) + | c, [] -> c in + let bl = array_map2 (remove_type avoid) consnargs bl in + ROrderedCase (dummy_loc,tag,pred,tomatch,bl,ref None) let rec detype tenv avoid env t = match kind_of_term (collapse_appl t) with @@ -291,8 +339,8 @@ let rec detype tenv avoid env t = let comp = computable p (annot.ci_pp_info.ind_nargs) in let ind = annot.ci_ind in let st = annot.ci_pp_info.style in - detype_case comp detype detype_eqn tenv avoid env ind st (Some p) c bl - + detype_case comp detype detype_eqn tenv avoid env ind st (Some p) + annot.ci_pp_info.ind_nargs c bl | Fix (nvn,recdef) -> detype_fix tenv avoid env nvn recdef | CoFix (n,recdef) -> detype_cofix tenv avoid env n recdef diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 13d37c843..5cf174875 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -29,7 +29,7 @@ val detype_case : 'a -> Rawterm.loc * Names.identifier list * Rawterm.cases_pattern list * Rawterm.rawconstr) -> env -> identifier list -> names_context -> inductive -> case_style -> - 'a option -> 'a -> 'a array -> rawconstr + 'a option -> int -> 'a -> 'a array -> rawconstr (* look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_renamed : env -> constr -> identifier -> int option diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 161c37ae8..ca25938b6 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -69,14 +69,20 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind = let indf = make_ind_family(ind,extended_rel_list nbprod lnamespar) in let lnamesar,_ = get_arity env indf in let ci = make_default_case_info env RegularStyle ind in + let depind = build_dependent_inductive env indf in + let deparsign = (Anonymous,None,depind)::lnamesar in + let p = (* mkRel nbprod *) it_mkLambda_or_LetIn_name env' - (lambda_create env' - (build_dependent_inductive env indf, - mkCase (ci, - mkRel (nbprod+nbargsprod), - mkRel 1, - rel_vect nbargsprod k))) - lnamesar + (appvect + (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod), + if dep then extended_rel_vect 0 deparsign + else extended_rel_vect 0 lnamesar)) + (if dep then deparsign else lnamesar) in + it_mkLambda_or_LetIn_name env' + (mkCase (ci, lift nbargsprod p, + mkRel 1, + rel_vect nbargsprod k)) + deparsign else let cs = lift_constructor (k+1) constrs.(k) in let t = build_branch_type env dep (mkRel (k+1)) cs in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index a64c55389..adc5932f1 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -239,6 +239,28 @@ let find_coinductive env sigma c = (* find appropriate names for pattern variables. Useful in the Case tactic. *) +let is_dep_predicate env kelim pred nodep_ar = + let rec srec env pval pt nodep_ar = + let pt' = whd_betadeltaiota env Evd.empty pt in + let pv' = whd_betadeltaiota env Evd.empty pval in + match kind_of_term pv', kind_of_term pt', kind_of_term nodep_ar with + | Lambda (na,t,b), Prod (_,_,a), Prod (_,_,a') -> + srec (push_rel_assum (na,t) env) b a a' + | _, Prod (na,t,a), Prod (_,_,a') -> + srec (push_rel_assum (na,t) env) (lift 1 pv') a a' + | Lambda (_,_,b), Prod (_,_,_), _ -> (*dependent (mkRel 1) b*) true + | _, Prod (_,_,_), _ -> true + | _ -> false in + srec env pred.uj_val pred.uj_type nodep_ar + +let is_dependent_elimination_predicate env pred indf = + let (ind,params) = indf in + let (_,mip) = Inductive.lookup_mind_specif env ind in + let kelim = mip.mind_kelim in + let arsign,s = get_arity env indf in + let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in + is_dep_predicate env kelim pred glob_t + let is_dep_arity env kelim predty nodep_ar = let rec srec pt nodep_ar = let pt' = whd_betadeltaiota env Evd.empty pt in @@ -256,7 +278,6 @@ let is_dependent_elimination env predty indf = let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in is_dep_arity env kelim predty glob_t - let set_names env n brty = let (ctxt,cl) = decompose_prod_n_assum n brty in it_mkProd_or_LetIn_name env cl ctxt @@ -277,7 +298,7 @@ let type_case_branches_with_names env indspec pj c = let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in let (mib,mip) = Inductive.lookup_mind_specif env ind in let params = list_firstn mip.mind_nparams args in - if is_dependent_elimination env pj.uj_type (ind,params) then + if is_dependent_elimination_predicate env pj (ind,params) then (set_pattern_names env ind lbrty, conclty) else (lbrty, conclty) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 92c581c71..d3479a846 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -237,15 +237,16 @@ let rec pat_of_raw metas vars = function Options.if_verbose Pp.warning "Cast not taken into account in constr pattern"; pat_of_raw metas vars c - | ROrderedCase (_,st,po,c,br) -> + | ROrderedCase (_,st,po,c,br,_) -> PCase ((None,st),option_app (pat_of_raw metas vars) po, pat_of_raw metas vars c, Array.map (pat_of_raw metas vars) br) - | RCases (loc,po,[c],brs) -> + | RCases (loc,(po,_),[c,_],brs) -> let sp = match brs with | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind | _ -> None in + (* When po disappears: switch to rtn type *) PCase ((sp,Term.RegularStyle),option_app (pat_of_raw metas vars) po, pat_of_raw metas vars c, Array.init (List.length brs) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0b665d4b2..e86d60c77 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -50,7 +50,7 @@ let transform_rec loc env sigma (pj,c,lf) indt = let (mib,mip) = lookup_mind_specif env ind in let recargs = mip.mind_recargs in let mI = mkInd ind in - let ci = make_default_case_info env MatchStyle ind in + let ci = make_default_case_info env (if Options.do_translate() then RegularStyle else MatchStyle) ind in let nconstr = Array.length mip.mind_consnames in if Array.length lf <> nconstr then (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in @@ -146,6 +146,8 @@ let inh_conv_coerce_to_tycon loc env isevars j = function | None -> j | Some typ -> inh_conv_coerce_to loc env isevars j typ +let push_rels vars env = List.fold_right push_rel vars env + (* let evar_type_case isevars env ct pt lft p c = let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c @@ -330,8 +332,7 @@ let rec pretype tycon env isevars lvar = function { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = type_app (subst1 j.uj_val) j'.uj_type } - (* Special Case for let constructions to avoid exponential behavior *) - | ROrderedCase (loc,st,po,c,[|f|]) when st <> MatchStyle -> + | RLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env isevars lvar c in let (IndType (indf,realargs) as indt) = try find_rectype env (evars_of isevars) cj.uj_type @@ -339,8 +340,67 @@ let rec pretype tycon env isevars lvar = function let cloc = loc_of_rawconstr c in error_case_not_inductive_loc cloc env (evars_of isevars) cj in + let cstrs = get_constructors env indf in + if Array.length cstrs <> 1 then + user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); + let cs = cstrs.(0) in + if List.length nal <> cs.cs_nargs then + user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); + let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) + (List.rev nal) cs.cs_args in + let env_f = push_rels fsign env in + let arsgn,_ = get_arity env indf in + let psign = (na,None,build_dependent_inductive env indf)::arsgn in + let nar = List.length arsgn in (match po with | Some p -> + let env_p = push_rels psign env in + let pj = pretype_type empty_valcon env_p isevars lvar p in + let ccl = nf_evar (evars_of isevars) pj.utj_val in + let fty = + let inst = (Array.to_list cs.cs_concl_realargs) + @[build_dependent_constructor cs] + in substl inst (liftn cs.cs_nargs nar ccl) in + let fj = pretype (mk_tycon fty) env_f isevars lvar d in + let f = it_mkLambda_or_LetIn fj.uj_val fsign in + let p = it_mkLambda_or_LetIn ccl psign in + let v = + let mis,_ = dest_ind_family indf in + let ci = make_default_case_info env LetStyle mis in + mkCase (ci, p, cj.uj_val,[|f|]) in + let cs = build_dependent_constructor cs in + { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } + + | None -> + let tycon = option_app (lift cs.cs_nargs) tycon in + let fj = pretype tycon env_f isevars lvar d in + let f = it_mkLambda_or_LetIn fj.uj_val fsign in + let ccl = nf_evar (evars_of isevars) fj.uj_type in + let ccl = + if noccur_between 1 cs.cs_nargs ccl then + lift (- cs.cs_nargs) ccl + else + error_cant_find_case_type_loc loc env (evars_of isevars) + cj.uj_val in + let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in + let v = + let mis,_ = dest_ind_family indf in + let ci = make_default_case_info env LetStyle mis in + mkCase (ci, p, cj.uj_val,[|f|] ) + in + { uj_val = v; uj_type = ccl }) + + (* Special Case for let constructions to avoid exponential behavior *) + | ROrderedCase (loc,st,po,c,[|f|],xx) when st <> MatchStyle -> + let cj = pretype empty_tycon env isevars lvar c in + let (IndType (indf,realargs) as indt) = + try find_rectype env (evars_of isevars) cj.uj_type + with Not_found -> + let cloc = loc_of_rawconstr c in + error_case_not_inductive_loc cloc env (evars_of isevars) cj + in + let j = match po with + | Some p -> let pj = pretype empty_tycon env isevars lvar p in let dep = is_dependent_elimination env pj.uj_type indf in let ar = @@ -425,9 +485,110 @@ let rec pretype tycon env isevars lvar = function let ci = make_default_case_info env st mis in mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,[|fv|] ) in - { uj_val = v; uj_type = rsty }) + { uj_val = v; uj_type = rsty } in + + (* Build the LetTuple form for v8 *) + let c = + let (ind,params) = dest_ind_family indf in + let rtntypopt, indnalopt = match po with + | None -> None, (Anonymous,None) + | Some p -> + let pj = pretype empty_tycon env isevars lvar p in + let dep = is_dependent_elimination env pj.uj_type indf in + let rec decomp_lam_force n avoid l p = + (* avoid is not exhaustive ! *) + if n = 0 then (List.rev l,p,avoid) else + match p with + | RLambda (_,(Name id as na),_,c) -> + decomp_lam_force (n-1) (id::avoid) (na::l) c + | RLambda (_,(Anonymous as na),_,c) -> + decomp_lam_force (n-1) avoid (na::l) c + | _ -> + let x = Nameops.next_ident_away (id_of_string "x") avoid in + decomp_lam_force (n-1) (x::avoid) (Name x :: l) + (* eta-expansion *) + (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in + let (nal,p,avoid) = + decomp_lam_force (List.length realargs) [] [] p in + let na,rtntyp,_ = + if dep then decomp_lam_force 1 avoid [] p + else [Anonymous],p,[] in + let intyp = + if List.for_all + (function + | Anonymous -> true + | Name id -> not (Cases.occur_rawconstr id rtntyp)) nal + then (* No dependency in realargs *) + None + else + let args = List.map (fun _ -> Anonymous) params @ nal in + Some (dummy_loc,ind,args) in + (Some rtntyp,(List.hd na,intyp)) in + let cs = (get_constructors env indf).(0) in + match indnalopt with + | (na,None) -> (* Represented as a let *) + let rec decomp_lam_force n avoid l p = + if n = 0 then (List.rev l,p) else + match p with + | RLambda (_,(Name id as na),_,c) -> + decomp_lam_force (n-1) (id::avoid) (na::l) c + | RLambda (_,(Anonymous as na),_,c) -> + decomp_lam_force (n-1) avoid (na::l) c + | _ -> + let x = Nameops.next_ident_away (id_of_string "x") avoid in + decomp_lam_force (n-1) (x::avoid) (Name x :: l) + (* eta-expansion *) + (let a = RVar (dummy_loc,x) in + match p with + | RApp (loc,p,l) -> RApp (loc,p,l@[a]) + | _ -> (RApp (dummy_loc,p,[a]))) in + let (nal,d) = decomp_lam_force cs.cs_nargs [] [] f in + RLetTuple (loc,nal,(na,rtntypopt),c,d) + | _ -> (* Represented as a match *) + let detype_eqn constr construct_nargs branch = + let name_cons = function + | Anonymous -> fun l -> l + | Name id -> fun l -> id::l in + let make_pat na avoid b ids = + PatVar (dummy_loc,na), + name_cons na avoid,name_cons na ids + in + let rec buildrec ids patlist avoid n b = + if n=0 then + (dummy_loc, ids, + [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], + b) + else + match b with + | RLambda (_,x,_,b) -> + let pat,new_avoid,new_ids = make_pat x avoid b ids in + buildrec new_ids (pat::patlist) new_avoid (n-1) b + + | RLetIn (_,x,_,b) -> + let pat,new_avoid,new_ids = make_pat x avoid b ids in + buildrec new_ids (pat::patlist) new_avoid (n-1) b + + | RCast (_,c,_) -> (* Oui, il y a parfois des cast *) + buildrec ids patlist avoid n c + + | _ -> (* eta-expansion *) + (* nommage de la nouvelle variable *) + let id = Nameops.next_ident_away (id_of_string "x") avoid in + let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in + let pat,new_avoid,new_ids = + make_pat (Name id) avoid new_b ids in + buildrec new_ids (pat::patlist) new_avoid (n-1) new_b + + in + buildrec [] [] [] construct_nargs branch in + let eqn = detype_eqn (ind,1) cs.cs_nargs f in + RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],[eqn]) + in + xx := Some c; + (* End building the v8 syntax *) + j - | ROrderedCase (loc,st,po,c,lf) -> + | ROrderedCase (loc,st,po,c,lf,x) -> let isrec = (st = MatchStyle) in let cj = pretype empty_tycon env isevars lvar c in let (IndType (indf,realargs) as indt) = @@ -503,6 +664,147 @@ let rec pretype tycon env isevars lvar = function mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val, Array.map (fun j-> j.uj_val) lfj) in + (* Build the Cases form for v8 *) + let c = + let (ind,params) = dest_ind_family indf in + let (mib,mip) = lookup_mind_specif env ind in + let recargs = mip.mind_recargs in + let mI = mkInd ind in + let nconstr = Array.length mip.mind_consnames in + let tyi = snd ind in + if isrec && mis_is_recursive_subset [tyi] recargs then + Some (Detyping.detype env [] (names_of_rel_context env) + (nf_evar (evars_of isevars) v)) + (* + let sigma = evars_of isevars in + let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in + let depFvec = Array.init mib.mind_ntypes init_depFvec in + (* build now the fixpoint *) + let lnames,_ = get_arity env indf in + let nar = List.length lnames in + let nparams = mip.mind_nparams in + let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in + let branches = + array_map3 + (fun f t reca -> + whd_beta + (Indrec.make_rec_branch_arg env sigma + (nparams,depFvec,nar+1) + f t reca)) + (Array.map (lift (nar+2)) lfv) constrs (dest_subterms recargs) + in + let ci = make_default_case_info env RegularStyle ind in + let deffix = + it_mkLambda_or_LetIn_name env + (lambda_create env + (applist (mI,List.append (List.map (lift (nar+1)) params) + (extended_rel_list 0 lnames)), + mkCase (ci, lift (nar+2) pj.uj_val, mkRel 1, branches))) + (lift_rel_context 1 lnames) + in + if noccurn 1 deffix then + Some + (Detyping.detype env [] (names_of_rel_context env) + (whd_beta (applist (pop deffix,realargs@[cj.uj_val])))) + else + let ind = applist (mI,(List.append + (List.map (lift nar) params) + (extended_rel_list 0 lnames))) in + let typPfix = + let rec aux = function + | (na,Some b,t)::l -> + | (na,None,t)::l -> RProd (dummy_loc,na, + | [] -> + it_mkProd_or_LetIn_name env + (prod_create env + (ind, + (if dep then + let ext_lnames = (Anonymous,None,ind)::lnames in + let args = extended_rel_list 0 ext_lnames in + whd_beta (applist (lift (nar+1) p, args)) + else + let args = extended_rel_list 1 lnames in + whd_beta (applist (lift (nar+1) p, args))))) + lnames in + let fix = + RRec (dummy_loc,RFix ([|nar|],0), + ([|(id_of_string "F")|],[|typPfix|],[|deffix|])) in + RApp (dummy_loc,fix,realargs@[c]) + (msgerrnl (str "Warning: could't translate Match"); None) +*) + else + let rtntypopt, indnalopt = match po with + | None -> None, (Anonymous,None) + | Some p -> + let rec decomp_lam_force n avoid l p = + (* avoid is not exhaustive ! *) + if n = 0 then (List.rev l,p,avoid) else + match p with + | RLambda (_,(Name id as na),_,c) -> + decomp_lam_force (n-1) (id::avoid) (na::l) c + | RLambda (_,(Anonymous as na),_,c) -> + decomp_lam_force (n-1) avoid (na::l) c + | _ -> + let x = Nameops.next_ident_away (id_of_string "x") avoid in + decomp_lam_force (n-1) (x::avoid) (Name x :: l) + (* eta-expansion *) + (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in + let (nal,p,avoid) = + decomp_lam_force (List.length realargs) [] [] p in + let na,rtntyopt,_ = + if dep then decomp_lam_force 1 avoid [] p + else [Anonymous],p,[] in + let args = List.map (fun _ -> Anonymous) params @ nal in + (Some rtntyopt,(List.hd na,Some (dummy_loc,ind,args))) in + + let detype_eqn constr construct_nargs branch = + let name_cons = function + | Anonymous -> fun l -> l + | Name id -> fun l -> id::l in + let make_pat na avoid b ids = + PatVar (dummy_loc,na), + name_cons na avoid,name_cons na ids + in + let rec buildrec ids patlist avoid n b = + if n=0 then + (dummy_loc, ids, + [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], + b) + else + match b with + | RLambda (_,x,_,b) -> + let pat,new_avoid,new_ids = make_pat x avoid b ids in + buildrec new_ids (pat::patlist) new_avoid (n-1) b + + | RLetIn (_,x,_,b) -> + let pat,new_avoid,new_ids = make_pat x avoid b ids in + buildrec new_ids (pat::patlist) new_avoid (n-1) b + + | RCast (_,c,_) -> (* Oui, il y a parfois des cast *) + buildrec ids patlist avoid n c + + | _ -> (* eta-expansion *) + (* nommage de la nouvelle variable *) + let id = Nameops.next_ident_away (id_of_string "x") avoid in + let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in + let pat,new_avoid,new_ids = + make_pat (Name id) avoid new_b ids in + buildrec new_ids (pat::patlist) new_avoid (n-1) new_b + + in + buildrec [] [] [] construct_nargs branch in + let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in + let get_consnarg j = + let typi = mis_nf_constructor_type (ind,mib,mip) (j+1) in + let _,t = decompose_prod_n_assum mip.mind_nparams typi in + List.rev (fst (decompose_prod_assum t)) in + let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in + let consnargsl = Array.map List.length consnargs in + let constructs = Array.init (Array.length lf) (fun i -> (ind,i+1)) in + let eqns = array_map3 detype_eqn constructs consnargsl lf in + Some (RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],Array.to_list eqns)) in + x := c; + (* End build the Cases form for v8 *) { uj_val = v; uj_type = rsty } diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 3e13cd861..bdb6914c2 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -67,10 +67,14 @@ type rawconstr = | RLambda of loc * name * rawconstr * rawconstr | RProd of loc * name * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr - | RCases of loc * rawconstr option * rawconstr list * + | RCases of loc * (rawconstr option * rawconstr option ref) * + (rawconstr * (name * (loc * inductive * name list) option) ref) list * (loc * identifier list * cases_pattern list * rawconstr) list + (* Rem: "ref" used for the v7->v8 translation only *) | ROrderedCase of loc * case_style * rawconstr option * rawconstr * - rawconstr array + rawconstr array * rawconstr option ref + | RLetTuple of loc * name list * (name * rawconstr option) * + rawconstr * rawconstr | RRec of loc * fix_kind * identifier array * rawconstr array * rawconstr array | RSort of loc * rawsort @@ -78,6 +82,10 @@ type rawconstr = | RCast of loc * rawconstr * rawconstr | RDynamic of loc * Dyn.t +let cases_predicate_names tml = + List.flatten (List.map (function + | (tm,{contents=(na,None)}) -> [na] + | (tm,{contents=(na,Some (_,_,nal))}) -> na::nal) tml) (*i - if PRec (_, names, arities, bodies) is in env then arities are typed in env too and bodies are typed in env enriched by the @@ -96,7 +104,8 @@ let loc = function | RProd (loc,_,_,_) -> loc | RLetIn (loc,_,_,_) -> loc | RCases (loc,_,_,_) -> loc - | ROrderedCase (loc,_,_,_,_) -> loc + | ROrderedCase (loc,_,_,_,_,_) -> loc + | RLetTuple (loc,_,_,_,_) -> loc | RRec (loc,_,_,_,_) -> loc | RCast (loc,_,_) -> loc | RSort (loc,_) -> loc @@ -112,11 +121,14 @@ let map_rawconstr f = function | RLambda (loc,na,ty,c) -> RLambda (loc,na,f ty,f c) | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c) | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c) - | RCases (loc,tyopt,tml,pl) -> - RCases (loc,option_app f tyopt,List.map f tml, + | RCases (loc,(tyopt,rtntypopt),tml,pl) -> + RCases (loc,(option_app f tyopt,ref (option_app f !rtntypopt)), + List.map (fun (tm,x) -> (f tm,x)) tml, List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl) - | ROrderedCase (loc,b,tyopt,tm,bv) -> - ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv) + | ROrderedCase (loc,b,tyopt,tm,bv,x) -> + ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv,ref (option_app f !x)) + | RLetTuple (loc,nal,(na,po),b,c) -> + RLetTuple (loc,nal,(na,option_app f po),f b,f c) | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv) | RCast (loc,c,t) -> RCast (loc,f c,f t) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x @@ -202,9 +214,17 @@ let rec subst_raw subst raw = if r1' == r1 && r2' == r2 then raw else RLetIn (loc,n,r1',r2') - | RCases (loc,ro,rl,branches) -> + | RCases (loc,(ro,rtno),rl,branches) -> let ro' = option_smartmap (subst_raw subst) ro - and rl' = list_smartmap (subst_raw subst) rl + and rtno' = ref (option_smartmap (subst_raw subst) !rtno) + and rl' = list_smartmap (fun (a,x as y) -> + let a' = subst_raw subst a in + let (n,topt) = !x in + let topt' = option_smartmap + (fun (loc,(sp,i),x as t) -> + let sp' = subst_kn subst sp in + if sp == sp' then t else (loc,(sp',i),x)) topt in + if a == a' && topt == topt' then y else (a',ref (n,topt'))) rl and branches' = list_smartmap (fun (loc,idl,cpl,r as branch) -> let cpl' = list_smartmap (subst_pat subst) cpl @@ -214,15 +234,22 @@ let rec subst_raw subst raw = branches in if ro' == ro && rl' == rl && branches' == branches then raw else - RCases (loc,ro',rl',branches') + RCases (loc,(ro',rtno'),rl',branches') - | ROrderedCase (loc,b,ro,r,ra) -> + | ROrderedCase (loc,b,ro,r,ra,x) -> let ro' = option_smartmap (subst_raw subst) ro and r' = subst_raw subst r and ra' = array_smartmap (subst_raw subst) ra in if ro' == ro && r' == r && ra' == ra then raw else - ROrderedCase (loc,b,ro',r',ra') - + ROrderedCase (loc,b,ro',r',ra',x) + + | RLetTuple (loc,nal,(na,po),b,c) -> + let po' = option_smartmap (subst_raw subst) po + and b' = subst_raw subst b + and c' = subst_raw subst c in + if po' == po && b' == b && c' == c then raw else + RLetTuple (loc,nal,(na,po),b,c) + | RRec (loc,fix,ida,ra1,ra2) -> let ra1' = array_smartmap (subst_raw subst) ra1 and ra2' = array_smartmap (subst_raw subst) ra2 in @@ -255,7 +282,8 @@ let loc_of_rawconstr = function | RProd (loc,_,_,_) -> loc | RLetIn (loc,_,_,_) -> loc | RCases (loc,_,_,_) -> loc - | ROrderedCase (loc,_,_,_,_) -> loc + | ROrderedCase (loc,_,_,_,_,_) -> loc + | RLetTuple (loc,_,_,_,_) -> loc | RRec (loc,_,_,_,_) -> loc | RSort (loc,_) -> loc | RHole (loc,_) -> loc diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index fbd01db9a..27bb76b69 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -65,10 +65,13 @@ type rawconstr = | RLambda of loc * name * rawconstr * rawconstr | RProd of loc * name * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr - | RCases of loc * rawconstr option * rawconstr list * + | RCases of loc * (rawconstr option * rawconstr option ref) * + (rawconstr * (name * (loc * inductive * name list) option) ref) list * (loc * identifier list * cases_pattern list * rawconstr) list | ROrderedCase of loc * case_style * rawconstr option * rawconstr * - rawconstr array + rawconstr array * rawconstr option ref + | RLetTuple of loc * name list * (name * rawconstr option) * + rawconstr * rawconstr | RRec of loc * fix_kind * identifier array * rawconstr array * rawconstr array | RSort of loc * rawsort @@ -76,6 +79,9 @@ type rawconstr = | RCast of loc * rawconstr * rawconstr | RDynamic of loc * Dyn.t +val cases_predicate_names : + (rawconstr * (name * (loc * inductive * name list) option) ref) list -> + name list (*i - if PRec (_, names, arities, bodies) is in env then arities are typed in env too and bodies are typed in env enriched by the diff --git a/states/MakeInitialNew.v b/states/MakeInitialNew.v index 8a321839b..02235e1b8 100644 --- a/states/MakeInitialNew.v +++ b/states/MakeInitialNew.v @@ -5,6 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Export Prelude; -Require Export Logic_Type; -Require Export Logic_TypeSyntax; +Require Export Prelude. +Require Export Logic_Type. +Require Export Logic_TypeSyntax. diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 2bd30c5eb..ddd5e4220 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -358,7 +358,7 @@ open Genarg let pr_hintbases _prc _prt = function | None -> str " with *" | Some [] -> mt () - | Some l -> str " with " ++ Util.prlist str l + | Some l -> str " with " ++ Util.prlist_with_sep spc str l ARGUMENT EXTEND hintbases TYPED AS preident_list_opt diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 37b8b3356..2a2db30f8 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -19,7 +19,9 @@ open Genarg let _ = Metasyntax.add_token_obj "<-" let _ = Metasyntax.add_token_obj "->" -let pr_orient _prc _prt = function true -> Pp.str " ->" | false -> Pp.str " <-" +let pr_orient _prc _prt = function + | true -> Pp.mt () + | false -> Pp.str " <-" ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient | [ "->" ] -> [ true ] diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 9462a7423..2efdabafc 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -408,8 +408,14 @@ let intern_constr {ltacvars=lfun; gsigma=sigma; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let c' = warn (Constrintern.interp_rawconstr_gen false sigma env [] - false (fst lfun,[])) c - in (c',if !strict_check then None else Some c) + false (fst lfun,[])) c in + begin if Options.do_translate () then try + (* Try to infer old case and type annotations *) + let _ = Pretyping.understand_gen_tcc sigma env [] None c' in + (* msgerrnl (str "Typage tactique OK");*) + () + with e -> (*msgerrnl (str "Warning: can't type tactic");*) () end; + (c',if !strict_check then None else Some c) (* Globalize bindings *) let intern_binding ist (loc,b,c) = @@ -2014,7 +2020,7 @@ let make_empty_glob_sign () = gsigma = Evd.empty; genv = Global.env() } let add_tacdef isrec tacl = - let isrec = if !Options.p1 then isrec else true in +(* let isrec = if !Options.p1 then isrec else true in*) let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in let ist = {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 33f8e488f..399134d11 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -237,13 +237,10 @@ let print_toplevel_error exc = (if is_pervasive_exn exc then (mt ()) else locstrm) ++ Cerrors.explain_exn exc -let is_term s = - if !Options.v7 then s="." else s=";" - (* Read the input stream until a dot is encountered *) let parse_to_dot = let rec dot st = match Stream.next st with - | ("", c) when is_term c -> () + | ("", ".") -> () | ("EOI", "") -> raise End_of_input | _ -> dot st in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1d2ccecbb..2b3b05b30 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -159,7 +159,7 @@ let show_intro all = (* "Print" commands *) let print_path_entry (s,l) = - (str s ++ tbrk (0,2) ++ str (string_of_dirpath l)) + (str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l)) let print_loadpath () = let l = Library.get_full_load_path () in @@ -703,7 +703,7 @@ let vernac_syntactic_definition id c = function | None -> syntax_definition id c | Some n -> let l = list_tabulate (fun _ -> (CHole (dummy_loc),None)) n in - let c = CApp (dummy_loc,(false,c),l) in + let c = CApp (dummy_loc,(None,c),l) in syntax_definition id c let vernac_declare_implicits locqid = function @@ -1172,7 +1172,7 @@ let interp c = match c with | VernacEndSegment id -> vernac_end_segment id - | VernacRecord (id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs + | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index e03658cfd..266e6c094 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -183,7 +183,8 @@ type vernac_expr = | VernacScheme of (identifier * bool * reference * sort_expr) list (* Gallina extensions *) - | VernacRecord of identifier with_coercion * simple_binder list + | VernacRecord of bool (* = Record or Structure *) + * identifier with_coercion * simple_binder list * constr_expr * identifier option * local_decl_expr with_coercion list | VernacBeginSection of identifier | VernacEndSegment of identifier diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index f8af13256..6d3974069 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -95,7 +95,7 @@ let pr_expl_args pr (a,expl) = let pr_opt_type pr = function | CHole _ -> mt () - | t -> cut () ++ str ":" ++ pr (if !Options.p1 then ltop else (latom,E)) t + | t -> cut () ++ str ":" ++ pr t let pr_opt_type_spc pr = function | CHole _ -> mt () @@ -103,7 +103,7 @@ let pr_opt_type_spc pr = function let pr_name = function | Anonymous -> str"_" - | Name id -> pr_id id + | Name id -> pr_id (Constrextern.v7_to_v8_id id) let pr_located pr (loc,x) = pr x @@ -139,67 +139,66 @@ let pr_binder pr (nal,t) = prlist_with_sep sep (pr_located pr_name) nal ++ pr_opt_type pr t) *) -(* Option 1a *) -let pr_oneb pr t na = - match t with - CHole _ -> pr_located pr_name na - | _ -> hov 1 - (str "(" ++ pr_located pr_name na ++ pr_opt_type pr t ++ str ")") -let pr_binder1 pr (nal,t) = - hov 0 (prlist_with_sep sep (pr_oneb pr t) nal) -let pr_binders1 pr bl = - hv 0 (prlist_with_sep sep (pr_binder1 pr) bl) +let surround p = str"(" ++ p ++ str")" -(* Option 1b *) -let pr_binder1 pr (nal,t) = +let pr_binder many pr (nal,t) = match t with - CHole _ -> prlist_with_sep sep (pr_located pr_name) nal - | _ -> hov 1 - (str "(" ++ prlist_with_sep sep (pr_located pr_name) nal ++ str ":" ++ - pr ltop t ++ str ")") - -let pr_binders1 pr bl = - hv 0 (prlist_with_sep sep (pr_binder1 pr) bl) - -let pr_opt_type' pr = function - | CHole _ -> mt () - | t -> cut () ++ str ":" ++ pr (latom,E) t - -let pr_prod_binders1 pr = function -(* | [nal,t] -> hov 1 (prlist_with_sep sep (pr_located pr_name) nal ++ pr_opt_type' pr t)*) - | bl -> pr_binders1 pr bl + CHole _ -> + prlist_with_sep sep (pr_located pr_name) nal + | _ -> + let s = + (prlist_with_sep sep (pr_located pr_name) nal ++ str ":" ++ pr t) in + hov 1 (if many then surround s else s) + +let pr_binder_among_many pr_c = function + | LocalRawAssum (nal,t) -> + pr_binder true pr_c (nal,t) + | LocalRawDef (na,c) -> + let c,topt = match c with + | CCast(_,c,t) -> c, t + | _ -> c, CHole dummy_loc in + hov 1 (surround + (pr_located pr_name na ++ pr_opt_type pr_c topt ++ + str":=" ++ cut() ++ pr_c c)) + +let pr_undelimited_binders pr_c = + prlist_with_sep sep (pr_binder_among_many pr_c) + +let pr_delimited_binders pr_c = function + | [LocalRawAssum (nal,t)] -> pr_binder false pr_c (nal,t) + | LocalRawAssum _ :: _ as bdl -> pr_undelimited_binders pr_c bdl + | _ -> assert false -(* Option 2 *) let pr_let_binder pr x a = hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ brk(0,1) ++ pr ltop a) -let pr_binder2 pr (nal,t) = - hov 0 ( - prlist_with_sep sep (pr_located pr_name) nal ++ - pr_opt_type pr t) - -let pr_binders2 pr bl = - hv 0 (prlist_with_sep sep (pr_binder2 pr) bl) - -let pr_prod_binder2 pr (nal,t) = - str "forall " ++ hov 0 ( - prlist_with_sep sep (pr_located pr_name) nal ++ - pr_opt_type pr t) ++ str "," - -let pr_prod_binders2 pr bl = - hv 0 (prlist_with_sep sep (pr_prod_binder2 pr) bl) - -(**) -let pr_binders pr = (if !Options.p1 then pr_binders1 else pr_binders2) pr -let pr_prod_binders pr bl = - if !Options.p1 then - str "!" ++ pr_prod_binders1 pr bl ++ str "." - else - pr_prod_binders2 pr bl - +let rec extract_prod_binders = function + | CLetIn (loc,na,b,c) -> + let bl,c = extract_prod_binders c in + LocalRawDef (na,b) :: bl, c + | CProdN (loc,[],c) -> + extract_prod_binders c + | CProdN (loc,(nal,t)::bl,c) -> + let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in + LocalRawAssum (nal,t) :: bl, c + | c -> [], c + +let rec extract_lam_binders = function + | CLetIn (loc,na,b,c) -> + let bl,c = extract_lam_binders c in + LocalRawDef (na,b) :: bl, c + | CLambdaN (loc,[],c) -> + extract_lam_binders c + | CLambdaN (loc,(nal,t)::bl,c) -> + let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in + LocalRawAssum (nal,t) :: bl, c + | c -> [], c + +(* let pr_arg_binders pr bl = if bl = [] then mt() else (spc() ++ pr_binders pr bl) +*) let pr_global vars ref = (* pr_global_env vars ref *) @@ -212,106 +211,20 @@ let split_lambda = function | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c)) | _ -> anomaly "ill-formed fixpoint body" -let split_product = function - | CArrow (loc,t,c) -> ((loc,Anonymous),t,c) - | CProdN (loc,[[na],t],c) -> (na,t,c) - | CProdN (loc,([na],t)::bl,c) -> (na,t,CProdN(loc,bl,c)) - | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c)) +let rename na na' t c = + match (na,na') with + | (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c) + | (_,Name id), (_,Anonymous) -> (na,t,c) + | _ -> (na',t,c) + +let split_product na' = function + | CArrow (loc,t,c) -> (na',t,c) + | CProdN (loc,[[na],t],c) -> rename na na' t c + | CProdN (loc,([na],t)::bl,c) -> rename na na' t (CProdN(loc,bl,c)) + | CProdN (loc,(na::nal,t)::bl,c) -> + rename na na' t (CProdN(loc,(nal,t)::bl,c)) | _ -> anomaly "ill-formed fixpoint body" -let rec extract_lam_binders c = - match c with - CLambdaN(loc,bl1,c') -> - let (bl,bd) = extract_lam_binders c' in - (bl1@bl, bd) - | _ -> ([],c) - -let rec extract_prod_binders c = - match c with - CProdN(loc,bl1,c') -> - let (bl,bd) = extract_prod_binders c' in - (bl1@bl, bd) - | _ -> ([],c) - -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 check_same_type 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 merge_binders (na1,ty1) (na2,ty2) = let na = match snd na1, snd na2 with @@ -325,9 +238,9 @@ let merge_binders (na1,ty1) (na2,ty2) = CHole _, _ -> ty2 | _, CHole _ -> ty1 | _ -> - check_same_type ty1 ty2; + Constrextern.check_same_type ty1 ty2; ty2 in - ([na],ty) + LocalRawAssum ([na],ty) let rec strip_domain bvar c = match c with @@ -358,13 +271,15 @@ let rec strip_domains (nal,ty) c = (* Re-share binders *) let rec factorize_binders = function | ([] | [_] as l) -> l - | (nal,ty)::((nal',ty')::l as l') -> - try - let _ = check_same_type ty ty' in - factorize_binders ((nal@nal',ty)::l) + | LocalRawAssum (nal,ty) as d :: (LocalRawAssum (nal',ty')::l as l') -> + (try + let _ = Constrextern.check_same_type ty ty' in + factorize_binders (LocalRawAssum (nal@nal',ty)::l) with _ -> - (nal,ty) :: factorize_binders l' + d :: factorize_binders l') + | d :: l -> d :: factorize_binders l +(* Extrac lambdas when a type constraint occurs *) let rec extract_def_binders c ty = match c with | CLambdaN(loc,bvar::lams,b) -> @@ -385,24 +300,29 @@ let rec split_fix n typ def = if n = 0 then ([],typ,def) else let (na,_,def) = split_lambda def in - let (_,t,typ) = split_product typ in + let (na,t,typ) = split_product na typ in let (bl,typ,def) = split_fix (n-1) typ def in - (([na],t)::bl,typ,def) + (LocalRawAssum ([na],t)::bl,typ,def) let pr_recursive_decl pr id b t c = pr_id id ++ b ++ pr_opt_type_spc pr t ++ str " :=" ++ brk(1,2) ++ pr ltop c +let name_of_binder = function + | LocalRawAssum (nal,_) -> nal + | LocalRawDef (_,_) -> [] + let pr_fixdecl pr (id,n,t0,c0) = let (bl,t,c) = extract_def_binders t0 c0 in let (bl,t,c) = if List.length bl <= n then split_fix (n+1) t0 c0 else (bl,t,c) in let annot = - let ids = List.flatten (List.map fst bl) in + let ids = List.flatten (List.map name_of_binder bl) in if List.length ids > 1 then spc() ++ str "{struct " ++ pr_name (snd (list_last ids)) ++ str"}" else mt() in - pr_recursive_decl pr id (str" " ++ hov 0 (pr_binders pr bl) ++ annot) t c + pr_recursive_decl pr id + (str" " ++ hov 0 (pr_undelimited_binders (pr ltop) bl) ++ annot) t c let pr_cofixdecl pr (id,t,c) = pr_recursive_decl pr id (mt ()) t c @@ -414,15 +334,35 @@ let pr_recursive pr_decl id = function prlist_with_sep (fun () -> fnl() ++ str "with ") pr_decl dl ++ fnl() ++ str "for " ++ pr_id id -let pr_annotation pr po = - match po with - None -> mt() - | Some p -> spc() ++ str "=> " ++ hov 0 (pr ltop p) +let pr_arg pr x = spc () ++ pr x -let pr_annotation2 pr po = +let is_var id = function + | CRef (Ident (_,id')) when id=id' -> true + | _ -> false + +let pr_case_item pr (tm,(na,indnalopt)) = + hov 0 (pr (lcast,E) tm ++ + (match na with + | Name id when not (is_var id tm) -> spc () ++ str "as " ++ pr_id id + | _ -> mt ()) ++ + (match indnalopt with + | None -> mt () + | Some (_,ind,nal) -> + spc () ++ str "in " ++ + hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal))) + +let pr_case_type pr po = match po with - None -> mt() - | Some p -> spc() ++ str "of type " ++ hov 0 (pr ltop p) + | None | Some (CHole _) -> mt() + | Some p -> spc() ++ str "return " ++ hov 0 (pr (lcast,E) p) + +let pr_return_type pr po = pr_case_type pr po + +let pr_simple_return_type pr na po = + (match na with + | Name id -> spc () ++ str "as " ++ pr_id id + | _ -> mt ()) ++ + pr_case_type pr po let pr_proj pr pr_app a f l = hov 0 (pr lsimple a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") @@ -451,57 +391,68 @@ let rec pr inherited a = larrow | CProdN _ -> let (bl,a) = extract_prod_binders a in - hv 0 (pr_prod_binders pr bl ++ spc() ++ pr ltop a), + hov 2 ( + str"forall" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++ + str "," ++ spc() ++ pr ltop a), lprod | CLambdaN _ -> let (bl,a) = extract_lam_binders a in - let left, mid = str"fun" ++ spc(), " =>" in hov 2 ( - left ++ pr_binders pr bl ++ - str mid ++ spc() ++ pr ltop a), + str"fun" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++ + str " =>" ++ spc() ++ pr ltop a), llambda | CLetIn (_,x,a,b) -> - let (bl,a) = extract_lam_binders a in hv 0 ( - hov 2 (str "let " ++ pr_located pr_name x ++ - pr_arg_binders pr bl ++ str " :=" ++ spc() ++ + hov 2 (str "let " ++ pr_located pr_name x ++ str " :=" ++ spc() ++ pr ltop a ++ str " in") ++ spc () ++ pr ltop b), lletin - | CAppExpl (_,(true,f),l) -> - let a,l = list_sep_last l in - pr_proj pr pr_appexpl a f l, lapp - | CAppExpl (_,(false,f),l) -> pr_appexpl pr f l, lapp - | CApp (_,(true,a),l) -> - let c,l = list_sep_last l in + | CAppExpl (_,(Some i,f),l) -> + let l1,l2 = list_chop i l in + let c,l1 = list_sep_last l1 in + pr_proj pr pr_appexpl c f l1 ++ + prlist (fun a -> spc () ++ pr (lapp,L) a) l2, lapp + | CAppExpl (_,(None,f),l) -> pr_appexpl pr f l, lapp + | CApp (_,(Some i,f),l) -> + let l1,l2 = list_chop i l in + let c,l1 = list_sep_last l1 in assert (snd c = None); - pr_proj pr pr_app (fst c) a l, lapp - | CApp (_,(false,a),l) -> pr_app pr a l, lapp - | CCases (_,po,c,eqns) -> + pr_proj pr pr_app (fst c) f l1 ++ + prlist (fun a -> spc () ++ pr_expl_args pr a) l2, lapp + | CApp (_,(None,a),l) -> pr_app pr a l, lapp + | CCases (_,(po,rtntypopt),c,eqns) -> v 0 - (hov 4 (str "match " ++ prlist_with_sep sep_v (pr ltop) c ++ - (if !Options.p1 then pr_annotation pr po else mt ()) ++ - str " with") ++ - prlist (pr_eqn pr) eqns ++ - (if !Options.p1 then mt () else pr_annotation2 pr po) - ++ spc() ++ - str "end"), + (hov 4 (str "match " ++ prlist_with_sep sep_v (pr_case_item pr) c + ++ pr_case_type pr rtntypopt ++ str " with") ++ + prlist (pr_eqn pr) eqns ++ spc() ++ str "end"), latom - | COrderedCase (_,_,po,c,[b1;b2]) -> + | CLetTuple (_,nal,(na,po),c,b) -> + hv 0 ( + str "let " ++ + hov 0 (str "(" ++ + prlist_with_sep sep_v pr_name nal ++ + str ")" ++ + pr_simple_return_type pr na po ++ str " :=" ++ + spc() ++ pr ltop c ++ str " in") ++ + spc() ++ pr ltop b), + lletin + + + | COrderedCase (_,st,po,c,[b1;b2]) when st = IfStyle -> (* On force les parenthèses autour d'un "if" sous-terme (même si le parsing est lui plus tolérant) *) hv 0 ( - str "if " ++ pr ltop c ++ pr_annotation pr po ++ spc () ++ + hov 1 (str "if " ++ pr ltop c ++ pr_return_type pr po) ++ spc () ++ hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++ hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2)), lif - | COrderedCase (_,_,po,c,[CLambdaN(_,[nal,_],b)]) -> + | COrderedCase (_,st,po,c,[CLambdaN(_,[nal,_],b)]) when st = LetStyle -> hv 0 ( str "let " ++ hov 0 (str "(" ++ prlist_with_sep sep_v (fun (_,n) -> pr_name n) nal ++ str ")" ++ - pr_annotation pr po ++ str " :=" ++ + pr_return_type pr po ++ str " :=" ++ spc() ++ pr ltop c ++ str " in") ++ spc() ++ pr ltop b), lletin @@ -509,7 +460,7 @@ let rec pr inherited a = hv 0 ( str (if style=MatchStyle then "old_match " else "match ") ++ pr ltop c ++ - pr_annotation pr po ++ + pr_return_type pr po ++ str " with" ++ brk (1,0) ++ hov 0 (prlist (fun b -> str "| ??? =>" ++ spc() ++ pr ltop b ++ fnl ()) bl) ++ @@ -530,21 +481,40 @@ let rec pr inherited a = if prec_less prec inherited then strm else str"(" ++ strm ++ str")" -let transf env vars c = +let rec strip_context n iscast t = + if n = 0 then + if iscast then match t with RCast (_,c,_) -> c | _ -> t else t + else match t with + | RLambda (_,_,_,c) -> strip_context (n-1) iscast c + | RProd (_,_,_,c) -> strip_context (n-1) iscast c + | RLetIn (_,_,_,c) -> strip_context (n-1) iscast c + | RCast (_,c,_) -> strip_context n false c + | _ -> anomaly "ppconstrnew: strip_context" + +let transf env n iscast c = if Options.do_translate() then - Constrextern.extern_rawconstr (Termops.vars_of_env env) - (Constrintern.for_grammar + let r = + Constrintern.for_grammar (Constrintern.interp_rawconstr_gen false Evd.empty env [] false - (vars,[])) - c) + ([],[])) + c in + begin try + (* Try to infer old case and type annotations *) + let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in + (*msgerrnl (str "Typage OK");*) () + with e -> (*msgerrnl (str "Warning: can't type")*) () end; + Constrextern.extern_rawconstr (Termops.vars_of_env env) + (strip_context n iscast r) else c -let pr_constr_env env c = pr lsimple (transf env [] c) -let pr_lconstr_env env c = pr ltop (transf env [] c) +let pr_constr_env env c = pr lsimple (transf env 0 false c) +let pr_lconstr_env env c = pr ltop (transf env 0 false c) let pr_constr c = pr_constr_env (Global.env()) c let pr_lconstr c = pr_lconstr_env (Global.env()) c -let pr_lconstr_vars vars c = pr ltop (transf (Global.env()) vars c) +let pr_lconstr_env_n env n b c = pr ltop (transf env n b c) + +let pr_binders = pr_undelimited_binders pr_lconstr let transf_pattern env c = if Options.do_translate() then @@ -561,24 +531,10 @@ let pr_rawconstr_env env c = let pr_lrawconstr_env env c = pr_lconstr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) -let anonymize_binder na c = - if Options.do_translate() then - Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env())) - (Reserve.anonymize_if_reserved na - (Constrintern.for_grammar - (Constrintern.interp_rawconstr Evd.empty (Global.env())) c)) - else c - -let pr_binders l = - prlist_with_sep sep - (fun (nal,t) -> prlist_with_sep sep - (fun (_,na as x) -> pr_oneb pr (anonymize_binder na t) x) nal) l - let pr_cases_pattern = pr_patt ltop let pr_occurrences prc (nl,c) = - prlist (fun n -> int n ++ spc ()) nl ++ - str"(" ++ prc c ++ str")" + prc c ++ prlist (fun n -> spc () ++ int n) nl let pr_qualid qid = str (string_of_qualid qid) @@ -604,7 +560,7 @@ let pr_metaid id = str"?" ++ pr_id id let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function | Red false -> str "red" | Hnf -> str "hnf" - | Simpl o -> str "simpl" ++ pr_opt (pr_occurrences pr_lconstr) o + | Simpl o -> str "simpl" ++ pr_opt (pr_occurrences pr_constr) o | Cbv f -> if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then str "compute" @@ -613,12 +569,13 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function | Lazy f -> hov 1 (str "lazy" ++ pr_red_flag pr_ref f) | Unfold l -> - hov 1 (str "unfold" ++ - prlist (fun (nl,qid) -> - prlist (pr_arg int) nl ++ spc () ++ pr_ref qid) l) + hov 1 (str "unfold " ++ + prlist_with_sep pr_coma (fun (nl,qid) -> + pr_ref qid ++ prlist (pr_arg int) nl) l) | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l) | Pattern l -> - hov 1 (str "pattern" ++ pr_arg (prlist (pr_occurrences pr_lconstr)) l) + hov 1 (str "pattern" ++ + pr_arg (prlist_with_sep pr_coma (pr_occurrences pr_constr)) l) | Red true -> error "Shouldn't be accessible from user" | ExtraRedExpr (s,c) -> diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli index cb2a1a677..40b122520 100644 --- a/translate/ppconstrnew.mli +++ b/translate/ppconstrnew.mli @@ -22,15 +22,16 @@ open Util open Genarg val extract_lam_binders : - constr_expr -> (name located list * constr_expr) list * constr_expr + constr_expr -> local_binder list * constr_expr val extract_prod_binders : - constr_expr -> (name located list * constr_expr) list * constr_expr + constr_expr -> local_binder list * constr_expr val extract_def_binders : constr_expr -> constr_expr -> - (name located list * constr_expr) list * constr_expr * constr_expr + local_binder list * constr_expr * constr_expr val split_fix : int -> constr_expr -> constr_expr -> - (name located list * constr_expr) list * constr_expr * constr_expr + local_binder list * constr_expr * constr_expr +val pr_binders : local_binder list -> std_ppcmds val prec_less : int -> int * Ppextend.parenRelation -> bool @@ -50,9 +51,8 @@ val pr_constr : constr_expr -> std_ppcmds val pr_lconstr : constr_expr -> std_ppcmds val pr_constr_env : env -> constr_expr -> std_ppcmds val pr_lconstr_env : env -> constr_expr -> std_ppcmds -val pr_lconstr_vars : identifier list -> constr_expr -> std_ppcmds +val pr_lconstr_env_n : env -> int -> bool -> constr_expr -> std_ppcmds val pr_cases_pattern : cases_pattern_expr -> std_ppcmds -val pr_binders : (name located list * constr_expr) list -> std_ppcmds val pr_may_eval : ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval -> std_ppcmds diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 6801aef28..80ac96492 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -23,6 +23,8 @@ open Genarg open Libnames open Pptactic +let pr_id id = pr_id (Constrextern.v7_to_v8_id id) + let pr_arg pr x = spc () ++ pr x let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp) @@ -48,7 +50,8 @@ let pr_binding prc = function let pr_esubst prc l = let pr_qhyp = function (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" - | (_,NamedHyp id,c) -> str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" + | (_,NamedHyp id,c) -> + str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" in prlist_with_sep spc pr_qhyp l @@ -171,8 +174,7 @@ let rec pr_tacarg_using_rule pr_gen = function | [], [] -> mt () | _ -> failwith "Inconsistent arguments of extended tactic" -let pr_then () = - if !Options.p1 then str " &" else str ";" +let pr_then () = str ";" open Closure diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 95055c43c..f8ece8cea 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -37,8 +37,20 @@ let pr_reference r = try match Nametab.extended_locate (snd (qualid_of_reference r)) with | TrueGlobal ref -> pr_reference (Constrextern.extern_reference dummy_loc Idset.empty ref) - | SyntacticDef sp -> - pr_reference r + | SyntacticDef kn -> + let is_coq_root d = + let d = repr_dirpath d in + d <> [] & string_of_id (list_last d) = "Coq" in + let dir,id = repr_path (sp_of_syntactic_definition kn) in + let r = + if (is_coq_root (Lib.library_dp()) or is_coq_root dir) then + (match string_of_id id with + | "refl_eqT" -> + Constrextern.extern_reference dummy_loc Idset.empty + (reference_of_constr (Coqlib.build_coq_eq_data ()).Coqlib.refl) + | _ -> r) + else r + in pr_reference r with Not_found -> error_global_not_found (snd (qualid_of_reference r)) @@ -96,6 +108,12 @@ let pr_entry_prec = function | Some Gramext.NonA -> str"NONA " | None -> mt() +let pr_prec = function + | Some Gramext.LeftA -> str", left associativity" + | Some Gramext.RightA -> str", right associativity" + | Some Gramext.NonA -> str", no associativity" + | None -> mt() + let pr_set_entry_type = function | ETIdent -> str"ident" | ETReference -> str"global" @@ -132,8 +150,8 @@ let pr_search a b pr_c = match a with let pr_locality local = if local then str "Local " else str "" let pr_class_rawexpr = function - | FunClass -> str"FUNCLASS" - | SortClass -> str"SORTCLASS" + | FunClass -> str"Funclass" + | SortClass -> str"Sortclass" | RefClass qid -> pr_reference qid let pr_option_ref_value = function @@ -224,7 +242,7 @@ let pr_with_declaration pr_c = function let rec pr_module_type pr_c = function | CMTEident qid -> pr_located pr_qualid qid | CMTEwith (mty,decl) -> - pr_module_type pr_c mty ++ spc() ++ str" with" ++ + pr_module_type pr_c mty ++ spc() ++ str" with" ++ spc() ++ pr_with_declaration pr_c decl let pr_of_module_type prc (mty,b) = @@ -271,29 +289,17 @@ let anonymize_binder na c = (Constrintern.interp_rawconstr Evd.empty (Global.env())) c)) else c -let sep_fields () = - if !Options.p1 then fnl () else str ";" ++ spc () - -let surround_binder p = - if !Options.p1 then str"(" ++ p ++ str")" else p +let surround p = str"(" ++ p ++ str")" let pr_binder pr_c ty na = match anonymize_binder (snd na) ty with CHole _ -> pr_located pr_name na | _ -> hov 1 - (surround_binder (pr_located pr_name na ++ str":" ++ cut() ++ pr_c ty)) - -let pr_valdecls pr_c = function - | LocalRawAssum (nal,c) -> - let sep = if !Options.p1 then spc else pr_tight_coma in - prlist_with_sep sep (pr_binder pr_c c) nal - | LocalRawDef (na,c) -> - hov 1 - (surround_binder (pr_located pr_name na ++ str":=" ++ cut() ++ pr_c c)) + (surround (pr_located pr_name na ++ str":" ++ cut() ++ pr_c ty)) -let pr_vbinders pr_c l = - hv 0 (prlist_with_sep spc (pr_valdecls pr_c) l) +let pr_vbinders l = + hv 0 (pr_binders l) let vars_of_valdecls l = function | LocalRawAssum (nal,c) -> @@ -310,15 +316,27 @@ let vars_of_binder l (nal,_) = let vars_of_binders = List.fold_left vars_of_binder [] +let anonymize_binder na c = + if Options.do_translate() then + Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env())) + (Reserve.anonymize_if_reserved na + (Constrintern.for_grammar + (Constrintern.interp_rawconstr Evd.empty (Global.env())) c)) + else c + let pr_sbinders sbl = if sbl = [] then mt () else - let bl = List.map (fun (id,c) -> ([(dummy_loc,Name id)],c)) sbl in + let bl = + List.map (fun (id,c) -> + let c = anonymize_binder (Name id) c in + LocalRawAssum ([(dummy_loc,Name id)],c)) sbl in pr_binders bl ++ spc () let pr_onescheme (id,dep,ind,s) = - pr_id id ++ str" :=" ++ spc() ++ - (if dep then str"Induction for" else str"Minimality for") - ++ spc() ++ pr_reference ind ++ spc() ++ str"Sort" ++ spc() ++ pr_sort s + hov 0 (pr_id id ++ str" :=") ++ spc() ++ + hov 0 ((if dep then str"Induction for" else str"Minimality for") + ++ spc() ++ pr_reference ind) ++ spc() ++ + hov 0 (str"Sort" ++ spc() ++ pr_sort s) let pr_class_rawexpr = function | FunClass -> str"FUNCLASS" @@ -340,14 +358,15 @@ let rec factorize = function | [] -> [] | (c,(x,t))::l -> match factorize l with - | (xl,t')::l' when t' = (c,t) & not !Options.p1 -> (x::xl,t')::l' + | (xl,t')::l' when t' = (c,t) -> (x::xl,t')::l' | l' -> ([x],(c,t))::l' let pr_ne_params_list pr_c l = - match factorize l with - | [params] -> surround_binder (pr_params pr_c params) - | l -> - prlist_with_sep spc (fun p -> str "(" ++ pr_params pr_c p ++ str ")") l + prlist_with_sep spc (fun p -> str "(" ++ pr_params pr_c p ++ str ")") +(* + prlist_with_sep pr_semicolon (pr_params pr_c) +*) + (factorize l) let pr_thm_token = function | Decl_kinds.Theorem -> str"Theorem" @@ -416,7 +435,7 @@ let pr_syntax_entry (p,rl) = str"level" ++ spc() ++ int p ++ str" :" ++ fnl() ++ prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_syntax_rule rl -let sep_end () = if !Options.p1 then str";" else str"." +let sep_end () = str"." (**************************************) (* Pretty printer for vernac commands *) @@ -449,7 +468,7 @@ let rec pr_vernac = function | VernacShow s -> let pr_showable = function | ShowGoal n -> str"Show" ++ pr_opt int n - | ShowGoalImplicitly n -> str"Show Implicits" ++ pr_opt int n + | ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n | ShowProof -> str"Show Proof" | ShowNode -> str"Show Node" | ShowScript -> str"Show Script" @@ -479,10 +498,16 @@ let rec pr_vernac = function | VernacVar id -> pr_id id (* Syntax *) - | VernacGrammar _ -> str"(* <Warning> : Grammar is replaced by Notation *)" + | VernacGrammar _ -> + msgerrnl (str"Warning : constr Grammar is discontinued; use Notation"); + str"(* <Warning> : Grammar is replaced by Notation *)" | VernacTacticGrammar l -> hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***) - | VernacSyntax (u,el) -> hov 1 (str"Syntax " ++ str u ++ spc() ++ - prlist_with_sep sep_v2 pr_syntax_entry el) (***) + | VernacSyntax (u,el) -> + msgerrnl (str"Warning : Syntax is discontinued; use Notation"); + str"(* Syntax is discontinued " ++ + hov 1 (str"Syntax " ++ str u ++ spc() ++ + prlist_with_sep sep_v2 pr_syntax_entry el) ++ + str " *)" | VernacOpenScope (local,sc) -> str "Open " ++ pr_locality local ++ str "Scope" ++ spc() ++ str sc | VernacDelimiters (sc,key) -> @@ -496,8 +521,11 @@ let rec pr_vernac = function let (a,p,s) = match ov8 with Some mv8 -> mv8 | None -> (a,p,s) in - hov 0 (str"Infix " ++ pr_locality local ++ pr_entry_prec a ++ int p - ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with + hov 0 (hov 0 (str"Infix " ++ pr_locality local + (* ++ pr_entry_prec a ++ int p ++ spc() *) + ++ qs s ++ spc() ++ pr_reference q) ++ spc() + ++ str "(at level " ++ int p ++ pr_prec a ++ str")" ++ + (match sn with | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) | VernacDistfix (local,a,p,s,q,sn) -> @@ -547,6 +575,20 @@ let rec pr_vernac = function str"Eval" ++ spc() ++ pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++ str" in" ++ spc() in + let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) in + let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) in + let rec abstract_rawconstr c = function + | [] -> c + | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl) + | LocalRawAssum (idl,t)::bl -> + List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl + (abstract_rawconstr c bl) in + let rec prod_rawconstr c = function + | [] -> c + | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl) + | LocalRawAssum (idl,t)::bl -> + List.fold_right (fun x b -> mkProdC([x],t,b)) idl + (prod_rawconstr c bl) in let pr_def_body = function | DefineBody (bl,red,c,d) -> let (bl2,body,ty) = match d with @@ -554,16 +596,25 @@ let rec pr_vernac = function let bl2,body = extract_lam_binders c in (bl2,body,mt()) | Some ty -> - let bl2,body,ty = extract_def_binders c ty in - (bl2,body, spc() ++ str":" ++ pr_lconstrarg ty) in + let bl2,body,ty' = extract_def_binders c ty in + (bl2,body, spc() ++ str":" ++ spc () ++ + pr_lconstr_env_n (Global.env()) + (List.length (vars_of_vbinders bl @ vars_of_vbinders bl2)) + false (prod_rawconstr ty bl)) in let bindings = - pr_ne_sep spc (pr_vbinders pr_lconstr) bl ++ + pr_ne_sep spc pr_vbinders bl ++ if bl2 = [] then mt() else (spc() ++ pr_binders bl2) in - let vars = vars_of_vbinders bl @ vars_of_binders bl2 in - let ppred = Some (pr_reduce red ++ pr_lconstr_vars vars body) in + let vars = vars_of_vbinders bl @ vars_of_vbinders bl2 in + let c',iscast = match d with None -> c, false + | Some d -> CCast (dummy_loc,c,d), true in + let ppred = + Some (pr_reduce red ++ + pr_lconstr_env_n (Global.env()) + (List.length vars) iscast (abstract_rawconstr c' bl)) + in (bindings,ty,ppred) | ProveBody (bl,t) -> - (pr_vbinders pr_lconstr bl, str" :" ++ pr_lconstrarg t, None) in + (pr_vbinders bl, str" :" ++ pr_lconstrarg t, None) in let (binds,typ,c) = pr_def_body b in hov 2 (pr_def_token e ++ spc() ++ pr_id id ++ binds ++ typ ++ (match c with @@ -574,7 +625,11 @@ let rec pr_vernac = function hov 1 (pr_thm_token ki ++ spc() ++ pr_id id ++ spc() ++ (match bl with | [] -> mt() - | _ -> pr_vbinders pr_lconstr bl ++ spc()) ++ str":" ++ spc() ++ pr_lconstr c ++ sep_end () ++ str "Proof") + | _ -> error "Statements with local binders no longer supported") +(* +pr_vbinders bl ++ spc()) +*) + ++ str":" ++ spc() ++ pr_lconstr c) ++ sep_end () ++ fnl() ++ str "Proof" | VernacEndProof (opac,o) -> (match o with | None -> if opac then str"Qed" else str"Defined" | Some (id,th) -> (match th with @@ -586,7 +641,8 @@ let rec pr_vernac = function (pr_assumption_token stre ++ spc() ++ pr_ne_params_list pr_lconstr l) | VernacInductive (f,l) -> - (* Copie simplifiée de command.ml pour recalculer les implicites *) + (* Copie simplifiée de command.ml pour recalculer les implicites, *) + (* les notations, et le contexte d'evaluation *) let lparams = match l with [] -> assert false | (_,_,la,_,_)::_ -> la in let nparams = List.length lparams and sigma = Evd.empty @@ -598,6 +654,32 @@ let rec pr_vernac = function (Termops.push_rel_assum (Name id,p) env, (Name id,None,p)::params)) (env0,[]) lparams in + + let (ind_env,ind_impls,arityl) = + List.fold_left + (fun (env, ind_impls, arl) (recname, _, _, arityc, _) -> + let arity = Constrintern.interp_type sigma env_params arityc in + let fullarity = + Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) in + let env' = Termops.push_rel_assum (Name recname,fullarity) env in + let impls = + if Impargs.is_implicit_args() + then Impargs.compute_implicits false env_params fullarity + else [] in + (env', (recname,impls)::ind_impls, (arity::arl))) + (env0, [], []) l + in + let lparnames = List.map (fun (na,_,_) -> na) params in + let notations = + List.map2 (fun (recname,ntnopt,_,_,_) ar -> + option_app (fun df -> + let larnames = + List.rev_append lparnames + (List.rev (List.map fst (fst (Term.decompose_prod ar)))) in + (recname,larnames,df)) ntnopt) + l arityl in + let ind_env_params = Environ.push_rel_context params ind_env in + let lparnames = List.map (fun (na,_,_) -> na) params in let impl_ntns = List.map (fun (recname,ntnopt,_,arityc,_) -> @@ -629,8 +711,8 @@ let rec pr_vernac = function let pr_constructor (coe,(id,c)) = hov 2 (pr_id id ++ str" " ++ - (if coe then str":>" else str":") ++ - pr_lconstrarg c) in + (if coe then str":>" else str":") ++ spc () ++ + pr_lconstr_env ind_env_params c) in let pr_constructor_list l = match l with | [] -> mt() | _ -> @@ -657,6 +739,7 @@ let rec pr_vernac = function | VernacFixpoint recs -> (* Copie simplifiée de command.ml pour recalculer les implicites *) + (* les notations, et le contexte d'evaluation *) let sigma = Evd.empty and env0 = Global.env() in let impl_ntns = List.map @@ -687,14 +770,24 @@ let rec pr_vernac = function Metasyntax.add_notation_interpretation df (AVar recname,larnames) scope) no) notations; + let rec_sign = + List.fold_left + (fun env ((recname,_,arityc,_),_) -> + let arity = Constrintern.interp_type sigma env0 arityc in + Environ.push_named (recname,None,arity) env) + (Global.env()) recs in + + let name_of_binder = function + | LocalRawAssum (nal,_) -> nal + | LocalRawDef (_,_) -> [] in let pr_onerec = function | (id,n,type_0,def0),ntn -> let (bl,def,type_) = extract_def_binders def0 type_0 in - let ids = List.flatten (List.map fst bl) in + let ids = List.flatten (List.map name_of_binder bl) in let (bl,def,type_) = if List.length ids <= n then split_fix (n+1) def0 type_0 else (bl,def,type_) in - let ids = List.flatten (List.map fst bl) in + let ids = List.flatten (List.map name_of_binder bl) in let annot = if List.length ids > 1 then spc() ++ str "{struct " ++ @@ -702,7 +795,9 @@ let rec pr_vernac = function else mt() in pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_ - ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++ pr_lconstr def + ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++ + pr_lconstr_env_n rec_sign (List.length (vars_of_vbinders bl)) + true (CCast (dummy_loc,def0,type_0)) in hov 1 (str"Fixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs) @@ -717,32 +812,32 @@ let rec pr_vernac = function prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) | VernacScheme l -> hov 2 (str"Scheme" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with") pr_onescheme l) + prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l) (* Gallina extensions *) - | VernacRecord ((oc,name),ps,s,c,fs) -> + | VernacRecord (b,(oc,name),ps,s,c,fs) -> let pr_record_field = function | (oc,AssumExpr (id,t)) -> - hov 1 (surround_binder (pr_id id ++ + hov 1 (pr_id id ++ (if oc then str" :>" else str" :") ++ spc() ++ - pr_lconstr t)) + pr_lconstr t) | (oc,DefExpr(id,b,opt)) -> (match opt with | Some t -> - hov 1 (surround_binder (pr_id id ++ + hov 1 (pr_id id ++ (if oc then str" :>" else str" :") ++ spc() ++ - pr_lconstr t ++ str" :=" ++ pr_lconstr b)) + pr_lconstr t ++ str" :=" ++ pr_lconstr b) | None -> - hov 1 (surround_binder (pr_id id ++ str" :=" ++ spc() ++ - pr_lconstr b))) in + hov 1 (pr_id id ++ str" :=" ++ spc() ++ + pr_lconstr b)) in hov 2 - (str"Record" ++ + (str (if b then "Record" else "Structure") ++ (if oc then str" > " else str" ") ++ pr_id name ++ spc() ++ pr_sbinders ps ++ str" :" ++ spc() ++ pr_lconstr s ++ str" := " ++ (match c with | None -> mt() - | Some sc -> pr_id sc) ++ spc() ++ str"{" ++ cut() ++ - hv 0 (prlist_with_sep sep_fields pr_record_field fs) - ++ str"}") + | Some sc -> pr_id sc) ++ + spc() ++ str"{" ++ + hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")) | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_id id) | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_id id) | VernacRequire (exp,spe,l) -> hov 2 @@ -789,7 +884,7 @@ let rec pr_vernac = function (* Solving *) | VernacSolve (i,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ - (if !Options.p1 then mt () else str "By ") ++ +(* str "By " ++*) (if deftac then mt() else str "!! ") ++ Options.with_option Options.translate_syntax (pr_raw_tactic_goal i) tac | VernacSolveExistential (i,c) -> @@ -833,9 +928,9 @@ let rec pr_vernac = function (Global.env()) body in hov 1 - ((if !Options.p1 then + (((*if !Options.p1 then (if rc then str "Recursive " else mt()) ++ - str "Tactic Definition " else + str "Tactic Definition " else*) (* Rec by default *) str "Ltac ") ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr @@ -851,9 +946,9 @@ let rec pr_vernac = function hov 2 (str"Syntactic Definition " ++ pr_id id ++ str" :=" ++ pr_lconstrarg c ++ spc() ++ str"|" ++ int n) | VernacDeclareImplicits (q,None) -> - hov 2 (str"Implicits" ++ spc() ++ pr_reference q) + hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) | VernacDeclareImplicits (q,Some l) -> - hov 1 (str"Implicits" ++ spc() ++ pr_reference q ++ spc() ++ + hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep int l ++ str"]") | VernacReserve (idl,c) -> hov 1 (str"Implicit Variable" ++ @@ -864,8 +959,17 @@ let rec pr_vernac = function spc() ++ prlist_with_sep sep pr_reference l) | VernacUnsetOption na -> hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) - | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> str"Set Implicit Arguments" - | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> str"Unset Implicit Arguments" + | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> str"Set Implicit Arguments" + ++ + (if !Options.translate_strict_impargs then + sep_end () ++ fnl () ++ str"Unset Strict Implicits" + else mt ()) + | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> + str"Set Strict Implicits" + ++ + (if !Options.translate_strict_impargs then + sep_end () ++ fnl () ++ str"Unset Implicit Arguments" + else mt ()) | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v) | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l)) | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l)) |