X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=5a5c7ba381f56216a15335cfecd93936602d1b39;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=b493edb6a22f295750a96141dd74f6a5d0a68385;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml index b493edb6a..5a5c7ba38 100644 --- a/matita/components/ng_tactics/nCicElim.ml +++ b/matita/components/ng_tactics/nCicElim.ml @@ -20,16 +20,16 @@ let fresh_name = let mk_id id = let id = if id = "_" then fresh_name () else id in - CicNotationPt.Ident (id,None) + NotationPt.Ident (id,None) ;; (*CSC: cut&paste from nCicReduction.split_prods, but does not check that the return type is a sort *) -let rec my_split_prods ~subst context n te = - match (n, NCicReduction.whd ~subst context te) with +let rec my_split_prods status ~subst context n te = + match (n, NCicReduction.whd status ~subst context te) with | (0, _) -> context,te | (n, NCic.Prod (name,so,ta)) -> - my_split_prods ~subst ((name,(NCic.Decl so))::context) (n - 1) ta + my_split_prods status ~subst ((name,(NCic.Decl so))::context) (n - 1) ta | (n, _) when n <= 0 -> context,te | (_, _) -> raise (Failure "my_split_prods") ;; @@ -38,48 +38,52 @@ let mk_appl = function [] -> assert false | [x] -> x - | CicNotationPt.Appl l1 :: l2 -> CicNotationPt.Appl (l1 @ l2) - | l -> CicNotationPt.Appl l + | NotationPt.Appl l1 :: l2 -> NotationPt.Appl (l1 @ l2) + | l -> NotationPt.Appl l ;; -let mk_elim uri leftno it (outsort,suffix) pragma = +let mk_elim status uri leftno it (outsort,suffix) pragma = let _,ind_name,ty,cl = it in let srec_name = ind_name ^ "_" ^ suffix in let rec_name = mk_id srec_name in let name_of_k id = mk_id ("H_" ^ id) in let p_name = mk_id "Q_" in - let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in + let params,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in let params = List.rev_map (function name,_ -> mk_id name) params in - let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in + let args,_sort = NCicReduction.split_prods status ~subst:[] [] (-1) ty in let args = List.rev_map (function name,_ -> mk_id name) args in let rec_arg = mk_id (fresh_name ()) in - let p_ty = + let mk_prods = List.fold_right - (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args - (CicNotationPt.Binder + (fun name res -> NotationPt.Binder (`Forall,(name,None),res)) in + let p_ty = mk_prods args + (NotationPt.Binder (`Forall, (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))), - CicNotationPt.Sort outsort)) in + NotationPt.Sort outsort)) in + let mk_arrs n = mk_prods (HExtlib.mk_list (mk_id "_") n) in let args = args @ [rec_arg] in let k_names = List.map (function _,name,_ -> name_of_k name) cl in + (* let final_params = List.map (function name -> name, None) params @ [p_name,Some p_ty] @ List.map (function name -> name, None) k_names @ List.map (function name -> name, None) args in + *) let cty = mk_appl (p_name :: args) in let ty = Some cty in - let branches = + let branches_with_args = List.map (function (_,name,ty) -> - let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in - let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in - let cargs_and_recursive_args = - List.rev_map - (function + let _,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in + let cargs,_ty= my_split_prods status ~subst:[] [] (-1) ty in + let cargs_recargs_nih = + List.fold_left + (fun (acc,nih) -> function _,NCic.Def _ -> assert false | name,NCic.Decl ty -> - let context,ty = my_split_prods ~subst:[] [] (-1) ty in + let context,ty = my_split_prods status ~subst:[] [] (-1) ty in match ty with | NCic.Const nref | NCic.Appl (NCic.Const nref::_) @@ -89,40 +93,54 @@ let mk_elim uri leftno it (outsort,suffix) pragma = -> let abs = List.rev_map (fun id,_ -> mk_id id) context in let name = mk_id name in - name, Some ( + (name, Some ( List.fold_right (fun id res -> - CicNotationPt.Binder (`Lambda,(id,None),res)) + NotationPt.Binder (`Lambda,(id,None),res)) abs - (CicNotationPt.Appl + (NotationPt.Appl (rec_name :: params @ [p_name] @ k_names @ - List.map (fun _ -> CicNotationPt.Implicit `JustOne) + List.map (fun _ -> NotationPt.Implicit `JustOne) (List.tl args) @ - [mk_appl (name::abs)]))) - | _ -> mk_id name,None - ) cargs in + [mk_appl (name::abs)]))))::acc, nih + 1 + | _ -> (mk_id name,None)::acc,nih + ) ([],0) cargs in + let cargs_and_recursive_args, nih = cargs_recargs_nih in let cargs,recursive_args = List.split cargs_and_recursive_args in let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in - CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), - mk_appl (name_of_k name :: cargs @ recursive_args) + (NotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), + mk_appl (name_of_k name :: cargs @ recursive_args)), (name,cargs, nih) ) cl in - let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in + let branches, branch_args = List.split branches_with_args in + let bo = NotationPt.Case (rec_arg,Some (ind_name,None),Some p_name,branches) in + let final_params = + List.map (function name -> name, None) params @ + [p_name,Some p_ty] @ + List.map (function name, cargs, nih -> + name_of_k name, + Some (mk_prods cargs (mk_arrs nih + (mk_appl + (p_name::HExtlib.mk_list (NotationPt.Implicit `JustOne) + (List.length args - 1) @ + [mk_appl (mk_id name :: params @ cargs)]))))) branch_args @ + List.map (function name -> name, None) args in let recno = List.length final_params in let where = recno - 1 in + let attrs = `Generated, `Definition, pragma in let res = - CicNotationPt.LetRec (`Inductive, - [final_params, (rec_name,ty), bo, where], rec_name) + NotationPt.LetRec (`Inductive, + [final_params, (rec_name,ty), bo, where], attrs) in (* prerr_endline (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) - 80 (CicNotationPres.render (fun _ -> None) + 80 (NotationPres.render (fun _ -> None) (TermContentPres.pp_ast res))); prerr_endline "#####"; let cobj = ("xxx", [], None, `Joint { @@ -136,7 +154,7 @@ let mk_elim uri leftno it (outsort,suffix) pragma = def_term = bo; def_type = List.fold_right - (fun x t -> CicNotationPt.Binder(`Forall,x,t)) + (fun x t -> NotationPt.Binder(`Forall,x,t)) final_params cty } ]; @@ -147,11 +165,9 @@ let mk_elim uri leftno it (outsort,suffix) pragma = prerr_endline ( (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) 80 - (CicNotationPres.mpres_of_box boxml))); + (NotationPres.mpres_of_box boxml))); *) - CicNotationPt.Theorem - (`Definition,srec_name, - CicNotationPt.Implicit `JustOne,Some res,pragma) + res ;; let ast_of_sort s = @@ -175,10 +191,10 @@ let ast_of_sort s = | _ -> assert false ;; -let mk_elims (uri,_,_,_,obj) = +let mk_elims status (uri,_,_,_,obj) = match obj with NCic.Inductive (true,leftno,[itl],_) -> - List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s) (`Elim s)) + List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s)) (NCic.Prop:: List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) | _ -> [] @@ -190,7 +206,7 @@ let mk_lambda = function [] -> assert false | [t] -> t - | l -> CicNotationPt.Appl l + | l -> NotationPt.Appl l ;; let rec count_prods = function NCic.Prod (_,_,t) -> 1 + count_prods t | _ -> 0;; @@ -204,36 +220,35 @@ let rec nth_prod projs n ty = (* this code should be unified with NTermCicContent.nast_of_cic0, but the two contexts have different types *) -let rec pp rels = - function +let pp (status: #NCic.status) = + let rec pp rels = + function NCic.Rel i -> List.nth rels (i - 1) - | NCic.Const _ as t -> - CicNotationPt.Ident - (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t,None) - | NCic.Sort s -> CicNotationPt.Sort (fst (ast_of_sort s)) + | NCic.Const _ as t -> NotationPt.NCic t + | NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s)) | NCic.Meta _ | NCic.Implicit _ -> assert false - | NCic.Appl l -> CicNotationPt.Appl (List.map (pp rels) l) + | NCic.Appl l -> NotationPt.Appl (List.map (pp rels) l) | NCic.Prod (n,s,t) -> let n = mk_id n in - CicNotationPt.Binder (`Pi, (n,Some (pp rels s)), pp (n::rels) t) + NotationPt.Binder (`Pi, (n,Some (pp rels s)), pp (n::rels) t) | NCic.Lambda (n,s,t) -> let n = mk_id n in - CicNotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t) - | NCic.LetIn (n,s,ty,t) -> + NotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t) + | NCic.LetIn (n,ty,s,t) -> let n = mk_id n in - CicNotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t) + NotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t) | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> let name = NUri.name_of_uri uri in let case_indty = Some (name, None) in let constructors, leftno = - let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in + let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in let _,_,_,cl = List.nth tys n in cl,leftno in let rec eat_branch n rels ty pat = match (ty, pat) with - | NCic.Prod (name, s, t), _ when n > 0 -> + | NCic.Prod (_name, _s, t), _ when n > 0 -> eat_branch (pred n) rels t pat | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') -> let cv, rhs = eat_branch 0 ((mk_id name)::rels) t t' in @@ -245,14 +260,16 @@ let rec pp rels = List.map2 (fun (_, name, ty) pat -> let capture_variables,rhs = eat_branch leftno rels ty pat in - CicNotationPt.Pattern (name, None, capture_variables), rhs + NotationPt.Pattern (name, None, capture_variables), rhs ) constructors patterns with Invalid_argument _ -> assert false in - CicNotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns) + NotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns) + in + pp ;; -let mk_projection leftno tyname consname consty (projname,_,_) i = +let mk_projection status leftno tyname consname consty (projname,_,_) i = let argsno = count_prods consty - leftno in let rec aux names ty leftno = match leftno,ty with @@ -260,19 +277,19 @@ let mk_projection leftno tyname consname consty (projname,_,_) i = let arg = mk_id "xxx" in let arg_ty = mk_appl (mk_id tyname :: List.rev names) in let bvar = mk_id "yyy" in - let underscore = CicNotationPt.Ident ("_",None),None in + let underscore = NotationPt.Ident ("_",None),None in let bvars = HExtlib.mk_list underscore i @ [bvar,None] @ HExtlib.mk_list underscore (argsno - i -1) in - let branch = CicNotationPt.Pattern (consname,None,bvars), bvar in + let branch = NotationPt.Pattern (consname,None,bvars), bvar in let projs,outtype = nth_prod [] i ty in let rels = List.map (fun name -> mk_appl (mk_id name :: List.rev names @ [arg])) projs @ names in - let outtype = pp rels outtype in - let outtype= CicNotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in - [arg, Some arg_ty], CicNotationPt.Case (arg,None,Some outtype,[branch]) + let outtype = pp status rels outtype in + let outtype= NotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in + [arg, Some arg_ty], NotationPt.Case (arg,None,Some outtype,[branch]) | _,NCic.Prod (name,_,t) -> let name = mk_id name in let params,body = aux (name::names) t (leftno - 1) in @@ -281,24 +298,24 @@ let mk_projection leftno tyname consname consty (projname,_,_) i = in let params,bo = aux [] consty leftno in let pprojname = mk_id projname in + let attrs = `Generated, `Definition, `Projection in let res = - CicNotationPt.LetRec (`Inductive, - [params, (pprojname,None), bo, leftno], pprojname) in + NotationPt.LetRec (`Inductive, + [params, (pprojname,None), bo, leftno], attrs) in (* prerr_endline (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) - 80 (CicNotationPres.render (fun _ -> None) + 80 (NotationPres.render (fun _ -> None) (TermContentPres.pp_ast res)));*) - CicNotationPt.Theorem - (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res,`Projection) + res ;; -let mk_projections (_,_,_,_,obj) = +let mk_projections status (_,_,_,_,obj) = match obj with NCic.Inductive (true,leftno,[_,tyname,_,[_,consname,consty]],(_,`Record fields)) -> - HExtlib.list_mapi (mk_projection leftno tyname consname consty) fields + HExtlib.list_mapi (mk_projection status leftno tyname consname consty) fields | _ -> [] ;;