For LetRec the pretty-printer is now in sync with the parser.
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"
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"
(* what to match, inductive type, out type, <pattern,action> 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
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
* 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} *)
| 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)
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
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 =
(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
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
| 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
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 ->
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
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 (
| `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
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) ->
| 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
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) ->
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
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 ] ];
]
];
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<def>>; OPT SYMBOL "|";
fst_constructors = LIST0 constructor SEP SYMBOL "|";
tl = OPT [ "with";
] ];
record_spec: [ [
- name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+ name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
fields = LIST0 [
name = IDENT ;
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
<entry id="grammar.rec_def">&rec_def;</entry>
<entry>::=</entry>
<entry>
- &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
+ &id; [&id;|<emphasis role="bold">_</emphasis>|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
</entry>
<entry />
</row>
<command>f</command> must be defined by means of tactics.</para>
<para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
</sect2>
+ <sect2 id="letrec">
+ <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
+ <titleabbrev>&TODO;</titleabbrev>
+ </sect2>
<sect2 id="inductive">
<title>[<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;]…]…
projects / helm.git / commitdiff