From 53b8e2af661ad4165aa0b1deccd0a7522d96ce2e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 30 Jan 2015 12:27:18 +0000 Subject: [PATCH] notation ast updated to comply with the toplevel let rec of ng_kernel --- matita/components/content/notationPp.ml | 43 +++++----- matita/components/content/notationPt.ml | 7 +- matita/components/content/notationUtil.ml | 32 +++---- .../content_pres/termContentPres.ml | 4 + .../components/disambiguation/disambiguate.ml | 59 ++++++------- .../grafite_parser/grafiteParser.ml | 18 +--- .../ng_disambiguation/grafiteDisambiguate.ml | 2 + .../ng_disambiguation/nCicDisambiguate.ml | 83 +++++++++---------- matita/components/ng_tactics/nCicElim.ml | 14 ++-- matita/components/syntax_extensions/.depend | 10 +-- 10 files changed, 128 insertions(+), 144 deletions(-) diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index d9ba51db0..d19bce283 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -116,28 +116,6 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = (* (pp_term ~pp_parens:true t2) *) (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t3) - | Ast.LetRec (kind, definitions, term) -> - let rec get_guard i = function - | [] -> (*assert false*) Ast.Implicit `JustOne - | [term, _] when i = 1 -> term - | _ :: tl -> get_guard (pred i) tl - in - let map (params, (id,typ), body, i) = - let typ = - match typ with - None -> Ast.Implicit `JustOne - | Some typ -> typ - in - sprintf "%s %s on %s: %s \\def %s" - (pp_term ~pp_parens:false term) - (String.concat " " (List.map (pp_capture_variable pp_term) params)) - (pp_term ~pp_parens:false (get_guard i params)) - (pp_term typ) (pp_term body) - in - sprintf "let %s %s in %s" - (match kind with `Inductive -> "rec" | `CoInductive -> "corec") - (String.concat " and " (List.map map definitions)) - (pp_term term) | Ast.Ident (name, Some []) | Ast.Ident (name, None) | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name | Ast.NRef nref -> NReference.string_of_reference nref @@ -328,6 +306,27 @@ let pp_obj pp_term = function | Ast.Record (params,name,ty,fields) -> "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ " \\def {" ^ pp_fields pp_term fields ^ "\n}" + | Ast.LetRec (kind, definitions, _) -> + let rec get_guard i = function + | [] -> assert false (* Ast.Implicit `JustOne *) + | [term, _] when i = 1 -> term + | _ :: tl -> get_guard (pred i) tl + in + let map (params, (id,typ), body, i) = + let typ = + match typ with + None -> assert false (* Ast.Implicit `JustOne *) + | Some typ -> typ + in + sprintf "%s %s on %s: %s \\def %s" + (pp_term id) + (String.concat " " (List.map (pp_capture_variable pp_term) params)) + (pp_term (get_guard i params)) + (pp_term typ) (pp_term body) + in + sprintf "let %s %s" + (match kind with `Inductive -> "rec" | `CoInductive -> "corec") + (String.concat " and " (List.map map definitions)) let rec pp_value (status: #NCic.status) = function | Env.TermValue t -> sprintf "$%s$" (pp_term status t) diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml index 087a43dde..52d433aa2 100644 --- a/matita/components/content/notationPt.ml +++ b/matita/components/content/notationPt.ml @@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option (** To be increased each time the term type below changes, used for "safe" * marshalling *) -let magic = 6 +let magic = 7 type term = (* CIC AST *) @@ -76,8 +76,6 @@ type term = (* what to match, inductive type, out type, list *) | Cast of term * term | LetIn of term capture_variable * term * term (* name, body, where *) - | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term - (* (params, name, body, decreasing arg) list, where *) | Ident of string * subst list option (* literal, substitutions. * Some [] -> user has given an empty explicit substitution list @@ -187,6 +185,8 @@ type 'term obj = *) | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list (** left parameters, name, type, fields *) + | LetRec of induction_kind * ('term capture_variable list * 'term capture_variable * 'term * int) list * NCic.f_attr + (* (params, name, body, decreasing arg) list, attributes *) (** {2 Standard precedences} *) @@ -194,4 +194,3 @@ let let_in_prec = 10 let binder_prec = 20 let apply_prec = 70 let simple_prec = 90 - diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml index 3683c0c0e..823febdb6 100644 --- a/matita/components/content/notationUtil.ml +++ b/matita/components/content/notationUtil.ml @@ -43,15 +43,6 @@ let visit_ast ?(special_k = fun _ -> assert false) | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2) | Ast.LetIn (var, t1, t3) -> Ast.LetIn (aux_capture_variable var, k t1, k t3) - | Ast.LetRec (kind, definitions, term) -> - let definitions = - List.map - (fun (params, var, ty, decrno) -> - List.map aux_capture_variable params, aux_capture_variable var, - k ty, decrno) - definitions - in - Ast.LetRec (kind, definitions, k term) | Ast.Ident (name, Some substs) -> Ast.Ident (name, Some (aux_substs substs)) | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs)) @@ -202,9 +193,6 @@ let meta_names_of_term term = | Ast.LetIn (_, t1, t3) -> aux t1 ; aux t3 - | Ast.LetRec (_, definitions, body) -> - List.iter aux_definition definitions ; - aux body | Ast.Uri (_, Some substs) -> aux_substs substs | Ast.Ident (_, Some substs) -> aux_substs substs | Ast.Meta (_, substs) -> aux_meta_substs substs @@ -232,10 +220,6 @@ let meta_names_of_term term = function Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars | Ast.Wildcard -> () - and aux_definition (params, var, term, decrno) = - List.iter aux_capture_var params ; - aux_capture_var var ; - aux term and aux_substs substs = List.iter (fun (_, term) -> aux term) substs and aux_meta_substs meta_substs = List.iter aux_opt meta_substs and aux_variable = function @@ -351,7 +335,7 @@ let fresh_id () = !fresh_index (* TODO ensure that names generated by fresh_var do not clash with user's *) - (* FG: "η" is not an identifier (it is rendered, but not be parsed) *) + (* FG: "η" is not an identifier (it is rendered, but not parsed) *) let fresh_name () = "eta" ^ string_of_int (fresh_id ()) let rec freshen_term ?(index = ref 0) term = @@ -375,9 +359,8 @@ let freshen_obj obj = let freshen_term = freshen_term ~index in let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in - let freshen_capture_variables = - List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t)) - in + let freshen_capture_variable (n, t) = freshen_term n, HExtlib.map_option freshen_term t in + let freshen_capture_variables = List.map freshen_capture_variable in match obj with | NotationPt.Inductive (params, indtypes) -> let indtypes = @@ -394,6 +377,15 @@ let freshen_obj obj = | NotationPt.Record (params, n, ty, fields) -> NotationPt.Record (freshen_capture_variables params, n, freshen_term ty, freshen_name_ty_b fields) + | NotationPt.LetRec (kind, definitions, attrs) -> + let definitions = + List.map + (fun (params, var, ty, decrno) -> + freshen_capture_variables params, freshen_capture_variable var, + freshen_term ty, decrno) + definitions + in + NotationPt.LetRec (kind, definitions, attrs) let freshen_term = freshen_term ?index:None diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml index 4a65e6ec9..49d9241b9 100644 --- a/matita/components/content_pres/termContentPres.ml +++ b/matita/components/content_pres/termContentPres.ml @@ -214,6 +214,7 @@ let pp_ast0 status t k = ]; break; k t ]) +(* | Ast.LetRec (rec_kind, funs, where) -> let rec_op = match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec" @@ -261,6 +262,7 @@ let pp_ast0 status t k = ((hvbox false false (fst_row :: List.flatten tl_rows @ [ break; keyword "in"; break; k where ]))) +*) | Ast.Implicit `JustOne -> builtin_symbol "?" | Ast.Implicit `Vector -> builtin_symbol "…" | Ast.Meta (n, l) -> @@ -594,9 +596,11 @@ let instantiate_level2 status env term = List.map (aux_branch env) patterns) | Ast.LetIn (var, t1, t3) -> Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3) +(* | Ast.LetRec (kind, definitions, body) -> Ast.LetRec (kind, List.map (aux_definition env) definitions, aux env body) +*) | Ast.Uri (name, None) -> Ast.Uri (name, None) | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs env substs)) diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml index 95d6082d0..58e600a42 100644 --- a/matita/components/disambiguation/disambiguate.ml +++ b/matita/components/disambiguation/disambiguate.ml @@ -261,34 +261,6 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function let where_dom = domain_of_term ~loc ~context:(string_of_name var :: context) where in body_dom @ type_dom @ where_dom - | Ast.LetRec (kind, defs, where) -> - let add_defs context = - List.fold_left - (fun acc (_, (var, _), _, _) -> string_of_name var :: acc - ) context defs in - let where_dom = domain_of_term ~loc ~context:(add_defs context) where in - let defs_dom = - List.fold_left - (fun dom (params, (_, typ), body, _) -> - let context' = - add_defs - (List.fold_left - (fun acc (var,_) -> string_of_name var :: acc) - context params) - in - List.rev - (snd - (List.fold_left - (fun (context,res) (var,ty) -> - string_of_name var :: context, - domain_of_term_option ~loc ~context ty @ res) - (add_defs context,[]) params)) - @ dom - @ domain_of_term_option ~loc ~context:context' typ - @ domain_of_term ~loc ~context:context' body - ) [] defs - in - defs_dom @ where_dom | Ast.Ident (name, subst) -> (try (* the next line can raise Not_found *) @@ -331,6 +303,10 @@ and domain_of_term_option ~loc ~context = function let domain_of_term ~context term = uniq_domain (domain_of_term ~context term) +let domain_of_term_option ~context = function + | None -> [] + | Some term -> domain_of_term ~context term + let domain_of_obj ~context ast = assert (context = []); match ast with @@ -376,6 +352,33 @@ let domain_of_obj ~context ast = (fun (context,res) (name,ty,_,_) -> Some name::context, res @ domain_of_term context ty ) (context_w_types,[]) fields) + | Ast.LetRec (kind, defs, _) -> + let add_defs context = + List.fold_left + (fun acc (_, (var, _), _, _) -> string_of_name var :: acc + ) context defs in + let defs_dom = + List.fold_left + (fun dom (params, (_, typ), body, _) -> + let context' = + add_defs + (List.fold_left + (fun acc (var,_) -> string_of_name var :: acc) + context params) + in + List.rev + (snd + (List.fold_left + (fun (context,res) (var,ty) -> + string_of_name var :: context, + domain_of_term_option ~context ty @ res) + (add_defs context,[]) params)) + @ dom + @ domain_of_term_option ~context:context' typ + @ domain_of_term ~context:context' body + ) [] defs + in + defs_dom let domain_of_obj ~context obj = uniq_domain (domain_of_obj ~context obj) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index ba58eda87..112970d3e 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -59,21 +59,8 @@ let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t) let default_associativity = Gramext.NonA let mk_rec_corec ind_kind defs loc = - let name,ty = - match defs with - | (params,(N.Ident (name, None), ty),_,_) :: _ -> - let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in - let ty = - List.fold_right - (fun var ty -> N.Binder (`Pi,var,ty) - ) params ty - in - name,ty - | _ -> assert false - in - let body = N.Ident (name,None) in - let attrs = `Provided, `Definition, `Regular in - (loc, N.Theorem(name, ty, Some (N.LetRec (ind_kind, defs, body)), attrs)) + let attrs = `Provided, `Definition, `Regular in + (loc, N.LetRec (ind_kind, defs, attrs)) let nmk_rec_corec ind_kind defs loc index = let loc,t = mk_rec_corec ind_kind defs loc in @@ -255,6 +242,7 @@ EXTEND | IDENT "width" | IDENT "size" | IDENT "nohyps" +(* | IDENT "timeout" *) ] ]; auto_params: [ diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml index 3601f4c44..baa28b2d6 100644 --- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml @@ -251,6 +251,8 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = | NotationPt.Inductive (_,(name,_,_,_)::_) | NotationPt.Record (_,name,_,_) -> name ^ ".ind" | NotationPt.Theorem (name,_,_,_) -> name ^ ".con" + | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con" + | NotationPt.LetRec _ | NotationPt.Inductive _ -> assert false in NUri.uri_of_string (baseuri ^ "/" ^ name) diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 62d05509c..24e69a43d 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -308,7 +308,6 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) in let cic_body = aux ~localize loc (cic_name :: context) body in NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) - | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term | NotationPt.Ident _ | NotationPt.Uri _ | NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed @@ -435,47 +434,11 @@ let interpretate_obj status | None,_ -> NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs) | Some bo,_ -> - (match bo with - | NotationPt.LetRec (kind, defs, _) -> - let inductive = kind = `Inductive in - let _,obj_context = - List.fold_left - (fun (i,acc) (_,(name,_),_,k) -> - (i+1, - (ncic_name_of_ident name, NReference.reference_of_spec uri - (if inductive then NReference.Fix (i,k,0) - else NReference.CoFix i)) :: acc)) - (0,[]) defs - in - let inductiveFuns = - List.map - (fun (params, (name, typ), body, decr_idx) -> - let add_binders kind t = - List.fold_right - (fun var t -> - NotationPt.Binder (kind, var, t)) params t - in - let cic_body = - interpretate_term status - ~obj_context ~context ~env ~uri:None ~is_path:false - (add_binders `Lambda body) - in - let cic_type = - interpretate_term_option status - ~obj_context:[] - ~context ~env ~uri:None ~is_path:false `Type - (HExtlib.map_option (add_binders `Pi) typ) - in - ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) - defs - in - NCic.Fixpoint (inductive,inductiveFuns,attrs) - | bo -> - let bo = - interpretate_term status - ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo - in - NCic.Constant ([],name,Some bo,ty',attrs))) + let bo = + interpretate_term status + ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo + in + NCic.Constant ([],name,Some bo,ty',attrs)) | NotationPt.Inductive (params,tyl) -> let context,params = let context,res = @@ -586,6 +549,42 @@ let interpretate_obj status let attrs = `Provided, `Record field_names in uri, height, [], [], NCic.Inductive (true,leftno,tyl,attrs) + | NotationPt.LetRec (kind, defs, attrs) -> + let inductive = kind = `Inductive in + let _,obj_context = + List.fold_left + (fun (i,acc) (_,(name,_),_,k) -> + (i+1, + (ncic_name_of_ident name, NReference.reference_of_spec uri + (if inductive then NReference.Fix (i,k,0) + else NReference.CoFix i)) :: acc)) + (0,[]) defs + in + let inductiveFuns = + List.map + (fun (params, (name, typ), body, decr_idx) -> + let add_binders kind t = + List.fold_right + (fun var t -> + NotationPt.Binder (kind, var, t)) params t + in + let cic_body = + interpretate_term status + ~obj_context ~context ~env ~uri:None ~is_path:false + (add_binders `Lambda body) + in + let cic_type = + interpretate_term_option status + ~obj_context:[] + ~context ~env ~uri:None ~is_path:false `Type + (HExtlib.map_option (add_binders `Pi) typ) + in + ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) + defs + in + let height = (* XXX calculate *) 0 in + uri, height, [], [], + NCic.Fixpoint (inductive,inductiveFuns,attrs) ;; let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml index 5a264c403..582f7353b 100644 --- a/matita/components/ng_tactics/nCicElim.ml +++ b/matita/components/ng_tactics/nCicElim.ml @@ -130,9 +130,10 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = 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 = NotationPt.LetRec (`Inductive, - [final_params, (rec_name,ty), bo, where], rec_name) + [final_params, (rec_name,ty), bo, where], attrs) in (* prerr_endline @@ -166,9 +167,7 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = (function x::_ -> x | _ -> assert false) 80 (NotationPres.mpres_of_box boxml))); *) - let attrs = `Generated, `Definition, pragma in - NotationPt.Theorem - (srec_name, NotationPt.Implicit `JustOne, Some res, attrs) + res ;; let ast_of_sort s = @@ -299,18 +298,17 @@ let mk_projection status 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 = NotationPt.LetRec (`Inductive, - [params, (pprojname,None), bo, leftno], pprojname) in + [params, (pprojname,None), bo, leftno], attrs) in (* prerr_endline (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) 80 (NotationPres.render (fun _ -> None) (TermContentPres.pp_ast res)));*) - let attrs = `Generated, `Definition, `Projection in - NotationPt.Theorem - (projname, NotationPt.Implicit `JustOne, Some res, attrs) + res ;; let mk_projections status (_,_,_,_,obj) = diff --git a/matita/components/syntax_extensions/.depend b/matita/components/syntax_extensions/.depend index 4b9bcffd4..119f13093 100644 --- a/matita/components/syntax_extensions/.depend +++ b/matita/components/syntax_extensions/.depend @@ -1,5 +1,5 @@ -utf8Macro.cmi : -utf8MacroTable.cmo : -utf8MacroTable.cmx : -utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: +utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi +utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi -- 2.39.2