From 774c8d18f41e71ae7e26a90d726d10a6f95de1fe Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 13 Oct 2006 16:53:54 +0000 Subject: [PATCH] New content level representations for LetRec, Inductive and CoInductive. For LetRec the pretty-printer is now in sync with the parser. --- .../components/acic_content/cicNotationPp.ml | 35 ++------ .../components/acic_content/cicNotationPt.ml | 8 +- .../acic_content/cicNotationUtil.ml | 16 ++-- .../acic_content/termAcicContent.ml | 54 ++++++++++-- .../cic_disambiguation/disambiguate.ml | 87 +++++++++++++------ .../grafite_parser/grafiteParser.ml | 20 ++--- helm/software/matita/help/C/sec_terms.xml | 6 +- 7 files changed, 149 insertions(+), 77 deletions(-) diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 785c8bd86..47bfe2748 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -114,33 +114,21 @@ let rec pp_term ?(pp_parens = true) t = sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) | Ast.LetRec (kind, definitions, term) -> - let strip i t = - let rec aux i l = function - | Ast.Binder (_, var, body) when i > 0 -> aux (pred i) (var :: l) body - | body -> List.rev l, body - in - aux i [] t - in let rec get_guard i = function | [] -> (*assert false*) Ast.Implicit | [term, _] when i = 1 -> term | _ :: tl -> get_guard (pred i) tl in - let map (var, body, i) = - let id, vars, typ, body = match var with - | term, Some typ -> - let pvars, pbody = strip i typ in - let _, bbody = strip i body in - term, pvars, pbody, bbody - | term, None -> - let pbody = Ast.Implicit in - let pvars, bbody = strip i body in - term, pvars, pbody, bbody - in + let map (params, (id,typ), body, i) = + let typ = + match typ with + None -> Ast.Implicit + | 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 vars)) - (pp_term ~pp_parens:false (get_guard i vars)) + (String.concat " " (List.map pp_capture_variable params)) + (pp_term ~pp_parens:false (get_guard i params)) (pp_term typ) (pp_term body) in sprintf "let %s %s in %s" @@ -271,12 +259,7 @@ let set_pp_term f = _pp_term := f let pp_params = function | [] -> "" - | params -> - " " ^ - String.concat " " - (List.map - (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ)) - params) + | params -> " " ^ String.concat " " (List.map pp_capture_variable params) let pp_flavour = function | `Definition -> "definition" diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 6ea1ec917..f6652f63f 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -75,8 +75,8 @@ type term = (* what to match, inductive type, out type, list *) | Cast of term * term | LetIn of capture_variable * term * term (* name, body, where *) - | LetRec of induction_kind * (capture_variable * term * int) list * term - (* (name, body, decreasing argument) list, where *) + | LetRec of induction_kind * (capture_variable list * 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 @@ -164,7 +164,7 @@ type cic_appl_pattern = type 'term inductive_type = string * bool * 'term * (string * 'term) list type obj = - | Inductive of (string * term) list * term inductive_type list + | Inductive of capture_variable list * term inductive_type list (** parameters, list of loc * mutual inductive types *) | Theorem of Cic.object_flavour * string * term * term option (** flavour, name, type, body @@ -174,7 +174,7 @@ type obj = * will be given in proof editing mode using the tactical language, * unless the flavour is an Axiom *) - | Record of (string * term) list * string * term * (string * term * bool * int) list + | Record of capture_variable list * string * term * (string * term * bool * int) list (** left parameters, name, type, fields *) (** {2 Standard precedences} *) diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index d9114b180..f331b79ca 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -40,7 +40,9 @@ let visit_ast ?(special_k = fun _ -> assert false) k = | Ast.LetRec (kind, definitions, term) -> let definitions = List.map - (fun (var, ty, n) -> aux_capture_variable var, k ty, n) + (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) @@ -213,7 +215,8 @@ let meta_names_of_term term = aux term and aux_pattern (head, _, vars) = List.iter aux_capture_var vars - and aux_definition (var, term, i) = + 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 @@ -367,6 +370,9 @@ 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 match obj with | CicNotationPt.Inductive (params, indtypes) -> let indtypes = @@ -374,15 +380,15 @@ let freshen_obj obj = (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors)) indtypes in - CicNotationPt.Inductive (freshen_name_ty params, indtypes) + CicNotationPt.Inductive (freshen_capture_variables params, indtypes) | CicNotationPt.Theorem (flav, n, t, ty_opt) -> let ty_opt = match ty_opt with None -> None | Some ty -> Some (freshen_term ty) in CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt) | CicNotationPt.Record (params, n, ty, fields) -> - CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty, - freshen_name_ty_b fields) + CicNotationPt.Record (freshen_capture_variables params, n, + freshen_term ty, freshen_name_ty_b fields) let freshen_term = freshen_term ?index:None diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 516d5f542..cda76ce09 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -198,28 +198,72 @@ let ast_of_acic0 term_info acic k = let defs = List.map (fun (_, n, decr_idx, ty, bo) -> - ((Ast.Ident (n, None), Some (k ty)), k bo, decr_idx)) + let params,bo = + let rec aux = + function + Cic.ALambda (_,name,so,ta) -> + let params,rest = aux ta in + (CicNotationUtil.name_of_cic_name name,Some (k so)):: + params, rest + | t -> [],t + in + aux bo + in + let ty = + let rec eat_pis = + function + 0,ty -> ty + | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta) + | n,ty -> + (* I should do a whd here, but I have no context *) + assert false + in + eat_pis ((List.length params),ty) + in + (params,(Ast.Ident (n, None), Some (k ty)), k bo, decr_idx)) funs in let name = try (match List.nth defs no with - | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n + | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n | _ -> assert false) with Not_found -> assert false in - idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None))) + idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None))) | Cic.ACoFix (id, no, funs) -> let defs = List.map (fun (_, n, ty, bo) -> - ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) + let params,bo = + let rec aux = + function + Cic.ALambda (_,name,so,ta) -> + let params,rest = aux ta in + (CicNotationUtil.name_of_cic_name name,Some (k so)):: + params, rest + | t -> [],t + in + aux bo + in + let ty = + let rec eat_pis = + function + 0,ty -> ty + | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta) + | n,ty -> + (* I should do a whd here, but I have no context *) + assert false + in + eat_pis ((List.length params),ty) + in + (params,(Ast.Ident (n, None), Some (k ty)), k bo, 0)) funs in let name = try (match List.nth defs no with - | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n + | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n | _ -> assert false) with Not_found -> assert false in diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index fb4c338a4..243f7c8bf 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -215,7 +215,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast | CicNotationPt.LetRec (kind, defs, body) -> let context' = List.fold_left - (fun acc ((name, _), _, _) -> + (fun acc (_, (name, _), _, _) -> CicNotationUtil.cic_name_of_name name :: acc) context defs in @@ -259,10 +259,16 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast in let inductiveFuns = List.map - (fun ((name, typ), body, decr_idx) -> - let cic_body = aux ~localize loc context' body in + (fun (params, (name, typ), body, decr_idx) -> + let add_binders kind t = + List.fold_right + (fun var t -> CicNotationPt.Binder (kind, var, t)) params t + in + let cic_body = + aux ~localize loc context' (add_binders `Lambda body) in let cic_type = - aux_option ~localize loc context (Some `Type) typ in + aux_option ~localize loc context (Some `Type) + (HExtlib.map_option (add_binders `Pi) typ) in let name = match CicNotationUtil.cic_name_of_name name with | Cic.Anonymous -> @@ -432,14 +438,17 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = let context,res = List.fold_left (fun (context,res) (name,t) -> - Cic.Name name :: context, - (name, interpretate_term context env None false t)::res + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res ) ([],[]) params in context,List.rev res in let add_params = - List.fold_right - (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in + List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in let name_to_uris = snd ( List.fold_left @@ -471,14 +480,18 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = let context,res = List.fold_left (fun (context,res) (name,t) -> - (Cic.Name name :: context), - (name, interpretate_term context env None false t)::res + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res ) ([],[]) params in context,List.rev res in let add_params = List.fold_right - (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in + (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in let ty' = add_params (interpretate_term context env None false ty) in let fields' = snd ( @@ -562,7 +575,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function | `Exists -> [ loc, Symbol ("exists", 0) ] | _ -> [] in - let type_dom = domain_rev_of_term_option loc context typ in + let type_dom = domain_rev_of_term_option ~loc context typ in let body_dom = domain_rev_of_term ~loc (CicNotationUtil.cic_name_of_name var :: context) body @@ -607,19 +620,31 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function in where_dom @ type_dom @ body_dom | CicNotationPt.LetRec (kind, defs, where) -> - let context' = + let add_defs context = List.fold_left - (fun acc ((var, typ), _, _) -> - CicNotationUtil.cic_name_of_name var :: acc) - context defs - in - let where_dom = domain_rev_of_term ~loc context' where in + (fun acc (_, (var, _), _, _) -> + CicNotationUtil.cic_name_of_name var :: acc + ) context defs in + let where_dom = domain_rev_of_term ~loc (add_defs context) where in let defs_dom = List.fold_left - (fun dom ((_, typ), body, _) -> + (fun dom (params, (_, typ), body, _) -> + let context' = + add_defs + (List.fold_left + (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc) + context params) + in domain_rev_of_term ~loc context' body @ - domain_rev_of_term_option loc context typ) - [] defs + domain_rev_of_term_option ~loc context typ @ + List.rev + (snd + (List.fold_left + (fun (context,res) (var,ty) -> + CicNotationUtil.cic_name_of_name var :: context, + res @ domain_rev_of_term_option ~loc context ty) + (add_defs context,[]) params)) + ) [] defs in where_dom @ defs_dom | CicNotationPt.Ident (name, subst) -> @@ -654,7 +679,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function | CicNotationPt.Magic _ | CicNotationPt.Variable _ -> assert false -and domain_rev_of_term_option loc context = function +and domain_rev_of_term_option ~loc context = function | None -> [] | Some t -> domain_rev_of_term ~loc context t @@ -681,12 +706,17 @@ let domain_of_obj ~context ast = let dom = List.fold_left (fun dom (_,ty) -> - domain_rev_of_term [] ty @ dom + match ty with + None -> dom + | Some ty -> domain_rev_of_term [] ty @ dom ) dom params in List.filter (fun (_,name) -> - not ( List.exists (fun (name',_) -> name = Id name') params + not ( List.exists (fun (name',_) -> + match CicNotationUtil.cic_name_of_name name' with + Cic.Anonymous -> false + | Cic.Name name' -> name = Id name') params || List.exists (fun (name',_,_,_) -> name = Id name') tyl) ) dom | CicNotationPt.Record (params,_,ty,fields) -> @@ -696,12 +726,17 @@ let domain_of_obj ~context ast = let dom = List.fold_left (fun dom (_,ty) -> - domain_rev_of_term [] ty @ dom + match ty with + None -> dom + | Some ty -> domain_rev_of_term [] ty @ dom ) (dom @ domain_rev_of_term [] ty) params in List.filter (fun (_,name) -> - not ( List.exists (fun (name',_) -> name = Id name') params + not ( List.exists (fun (name',_) -> + match CicNotationUtil.cic_name_of_name name' with + Cic.Anonymous -> false + | Cic.Name name' -> name = Id name') params || List.exists (fun (name',_,_,_) -> name = Id name') fields) ) dom in diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index af185a63e..9b9a5da22 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -61,12 +61,6 @@ type by_continuation = EXTEND GLOBAL: term statement; - arg: [ - [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; - SYMBOL ":"; ty = term; RPAREN -> names,ty - | name = IDENT -> [name],Ast.Implicit - ] - ]; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; tactic_term: [ [ t = term LEVEL "90N" -> t ] ]; ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ]; @@ -360,7 +354,7 @@ EXTEND ] ]; inductive_spec: [ [ - fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; + fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars; SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; fst_constructors = LIST0 constructor SEP SYMBOL "|"; tl = OPT [ "with"; @@ -382,7 +376,7 @@ EXTEND ] ]; record_spec: [ [ - name = IDENT; params = LIST0 [ arg = arg -> arg ] ; + name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ; SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; fields = LIST0 [ name = IDENT ; @@ -551,8 +545,14 @@ EXTEND defs = CicNotationParser.let_defs -> let name,ty = match defs with - | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty - | ((Ast.Ident (name, None), None),_,_) :: _ -> + | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ -> + let ty = + List.fold_right + (fun var ty -> Ast.Binder (`Pi,var,ty) + ) params ty + in + name,ty + | (_,(Ast.Ident (name, None), None),_,_) :: _ -> name, Ast.Implicit | _ -> assert false in diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index f5ac2b3ec..65000b9ba 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -198,7 +198,7 @@ &rec_def; ::= - &id; [&id;|(&id;[,&term;]… :&term;)]… + &id; [&id;|_|(&id;[,&id;]… :&term;)]… @@ -417,6 +417,10 @@ f must be defined by means of tactics. Notice that the command is equivalent to theorem f: T ≝ t. + + <emphasis role="bold">letrec</emphasis> &TODO; + &TODO; + [<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]… [<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]… -- 2.39.2