(* (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
| 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)
(** To be increased each time the term type below changes, used for "safe"
* marshalling *)
-let magic = 6
+let magic = 7
type term =
(* CIC AST *)
(* what to match, inductive type, out type, <pattern,action> 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
*)
| 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} *)
let binder_prec = 20
let apply_prec = 70
let simple_prec = 90
-
| 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))
| 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
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
!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 =
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 =
| 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
];
break;
k t ])
+(*
| Ast.LetRec (rec_kind, funs, where) ->
let rec_op =
match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
((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) ->
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))
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 *)
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
(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)
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
| IDENT "width"
| IDENT "size"
| IDENT "nohyps"
+(* | IDENT "timeout" *)
]
];
auto_params: [
| 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)
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
| 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 =
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
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
(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 =
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) =
-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
projects / helm.git / commitdiff