Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Ppopen Utilopen Esubstopen Namesopen Environopen Declarationsopen Constr
type reloc_table = (int * int) array
type case_annot = case_info * reloc_table * Declarations.recursivity_kind
type 'v node =| Lrel of Name.t * int| Lvar of Id.t| Levar of Evar.t * 'v lambda array (* arguments *)| Lprod of 'v lambda * 'v lambda| Llam of Name.t binder_annot array * 'v lambda| Llet of Name.t binder_annot * 'v lambda * 'v lambda| Lapp of 'v lambda * 'v lambda array| Lconst of pconstant| Lproj of Projection.Repr.t * 'v lambda| Lprim of pconstant * CPrimitives.t * 'v lambda array| Lcase of case_annot * 'v lambda * 'v lambda * 'v lam_branches (* annotations, term being matched, accu, branches *)| Lfix of (int array * inductive array * int) * 'v fix_decl| Lcofix of int * 'v fix_decl| Lint of int| Lparray of 'v lambda array * 'v lambda| Lmakeblock of inductive * int * 'v lambda array (* inductive name, constructor tag, arguments *)| Luint of Uint63.t| Lfloat of Float64.t| Lstring of Pstring.t| Lval of 'v| Lsort of Sorts.t| Lind of pinductive
and 'v lam_branches = { constant_branches : 'v lambda array; nonconstant_branches : (Name.t binder_annot array * 'v lambda) array }
and 'v fix_decl = Name.t binder_annot array * 'v lambda array * 'v lambda array
and 'v lambda = { node : 'v node }
type evars = { evars_val : CClosure.evar_handler }
let empty_evars env = { evars_val = CClosure.default_evar_handler env }
(** Printing **)
let pr_annot x = Name.print x.Context.binder_name
let pp_names ids = prlist_with_sep (fun _ -> brk(1,1)) pr_annot (Array.to_list ids)
let pp_rel name n = Name.print name ++ str "##" ++ int n
let pr_con sp = str(Names.Id.to_string (Constant.label sp))
let rec pp_lam lam = match lam.node with | Lrel (id,n) -> pp_rel id n | Lvar id -> Id.print id | Levar (evk, args) -> hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")") | Lprod(dom,codom) -> hov 1 (str "forall(" ++ pp_lam dom ++ str "," ++ spc() ++ pp_lam codom ++ str ")") | Llam(ids,body) -> hov 1 (str "(fun " ++ pp_names ids ++ str " =>" ++ spc() ++ pp_lam body ++ str ")") | Llet(id,def,body) -> hov 0 (str "let " ++ pr_annot id ++ str ":=" ++ pp_lam def ++ str " in" ++ spc() ++ pp_lam body) | Lapp(f, args) -> hov 1 (str "(" ++ pp_lam f ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") | Lconst (kn,_) -> pr_con kn | Lcase(_annot, t, a, branches) -> let ic = ref (-1) in let ib = ref 0 in v 0 (str"<" ++ pp_lam t ++ str">" ++ cut() ++ str "Case" ++ spc () ++ pp_lam a ++ spc() ++ str "of" ++ cut() ++ v 0 ((prlist_with_sep (fun _ -> str "") (fun c -> cut () ++ str "| " ++ int (incr ic; !ic) ++ str " => " ++ pp_lam c) (Array.to_list branches.constant_branches)) ++ (prlist_with_sep (fun _ -> str "") (fun (ids,c) -> cut () ++ str "| " ++ int (incr ib; !ib) ++ str " " ++ pp_names ids ++ str " => " ++ pp_lam c) (Array.to_list branches.nonconstant_branches))) ++ cut() ++ str "end") | Lfix ((t, _, i), (lna, tl, bl)) -> let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in hov 1 (str"fix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> pr_annot na ++ str"/" ++ int i ++ str":" ++ pp_lam ty ++ cut() ++ str":=" ++ pp_lam bd) (Array.to_list fixl)) ++ str"}")
| Lcofix (i,(lna,tl,bl)) -> let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in hov 1 (str"cofix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,ty,bd) -> pr_annot na ++ str":" ++ pp_lam ty ++ cut() ++ str":=" ++ pp_lam bd) (Array.to_list fixl)) ++ str"}") | Lparray (args, def) -> hov 1 (str "(array " ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ spc () ++ str "|" ++ spc () ++ pp_lam def ++ str")") | Lmakeblock(_, tag, args) -> hov 1 (str "(makeblock " ++ int tag ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") | Luint i -> str (Uint63.to_string i) | Lfloat f -> str (Float64.to_string f) | Lstring s -> str (Printf.sprintf "%S" (Pstring.to_string s)) | Lval _ -> str "values" | Lsort s -> Sorts.raw_pr s | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i | Lprim ((kn,_u),_op,args) -> hov 1 (str "(PRIM " ++ pr_con kn ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") | Lproj(p,arg) -> hov 1 (str "(proj " ++ str "{" ++ Projection.Repr.print p ++ str "}" ++ spc () ++ pp_lam arg ++ str ")") | Lint i -> Pp.(str "(int:" ++ int i ++ str ")")
(*s Constructors *)
let mknode t = { node = t }
let node t = t.node
let mkLapp f args = if Array.is_empty args then f else match f.node with | Lapp(f', args') -> mknode @@ Lapp (f', Array.append args' args) | _ -> mknode @@ Lapp(f, args)
let mkLlam ids body = if Array.is_empty ids then body else match body.node with | Llam(ids', body) -> mknode @@ Llam(Array.append ids ids', body) | _ -> mknode @@ Llam(ids, body)
(* Hack: brutally pierce through the abstraction of PArray *)let unsafe_mkPArray args def = let dummy = KerName.make (ModPath.MPfile DirPath.empty) (Id.of_string "dummy") in let dummy = (MutInd.make1 dummy, 0) in let ar = mknode @@ Lmakeblock (dummy, 0, args) in let kind = mknode @@ Lmakeblock (dummy, 0, [|ar; def|]) in (* Parray.Array *) mknode @@ Lmakeblock (dummy, 0, [|kind|]) (* the reference *)
(* Same as above but with a blob instead of a block *)let unsafe_mkPArray_val v def = let dummy = KerName.make (ModPath.MPfile DirPath.empty) (Id.of_string "dummy") in let dummy = (MutInd.make1 dummy, 0) in let ar = mknode @@ Lval v in let kind = mknode @@ Lmakeblock (dummy, 0, [|ar; def|]) in (* Parray.Array *) mknode @@ Lmakeblock (dummy, 0, [|kind|]) (* the reference *)
let decompose_Llam lam = match lam.node with | Llam(ids,body) -> ids, body | _ -> [||], lam
let rec decompose_Llam_Llet lam = match lam.node with | Llam(ids,body) -> let vars, body = decompose_Llam_Llet body in Array.fold_right (fun x l -> (x, None) :: l) ids vars, body | Llet(id,def,body) -> let vars, body = decompose_Llam_Llet body in (id,Some def) :: vars, body | _ -> [], lam
let decompose_Llam_Llet lam = let vars, body = decompose_Llam_Llet lam in Array.of_list vars, body
(* A generic map function *)
let map_lam_with_binders g f n lam = match lam.node with | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ | Lfloat _ | Lstring _ -> lam | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else mknode @@ Levar (evk, args') | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in if dom == dom' && codom == codom' then lam else mknode @@ Lprod(dom',codom') | Llam(ids,body) -> let body' = f (g (Array.length ids) n) body in if body == body' then lam else mkLlam ids body' | Llet(id,def,body) -> let def' = f n def in let body' = f (g 1 n) body in if body == body' && def == def' then lam else mknode @@ Llet(id,def',body') | Lapp(fct,args) -> let fct' = f n fct in let args' = Array.Smart.map (f n) args in if fct == fct' && args == args' then lam else mkLapp fct' args' | Lcase (annot, t, a, branches) -> let const = branches.constant_branches in let nonconst = branches.nonconstant_branches in let t' = f n t in let a' = f n a in let const' = Array.Smart.map (f n) const in let on_b b = let (ids,body) = b in let body' = f (g (Array.length ids) n) body in if body == body' then b else (ids,body') in let nonconst' = Array.Smart.map on_b nonconst in let branches' = if const == const' && nonconst == nonconst' then branches else { constant_branches = const'; nonconstant_branches = nonconst' } in if t == t' && a == a' && branches == branches' then lam else mknode @@ Lcase(annot, t', a', branches') | Lfix(init,(ids,ltypes,lbodies)) -> let ltypes' = Array.Smart.map (f n) ltypes in let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else mknode @@ Lfix(init,(ids,ltypes',lbodies')) | Lcofix(init,(ids,ltypes,lbodies)) -> let ltypes' = Array.Smart.map (f n) ltypes in let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else mknode @@ Lcofix(init,(ids,ltypes',lbodies')) | Lparray (args, def) -> let args' = Array.Smart.map (f n) args in let def' = f n def in if args == args' && def == def' then lam else mknode @@ Lparray (args', def') | Lmakeblock (inds, tag, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else mknode @@ Lmakeblock (inds, tag,args') | Lprim(kn,op,args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else mknode @@ Lprim(kn,op,args') | Lproj(p,arg) -> let arg' = f n arg in if arg == arg' then lam else mknode @@ Lproj(p,arg')
(* Free rels *)
let free_rels lam = let rec aux k accu lam = match node lam with | Lrel (_, n) -> if n >= k then Int.Set.add (n - k + 1) accu else accu | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ | Lfloat _ | Lstring _ -> accu | Levar (_, args) -> Array.fold_left (fun accu lam -> aux k accu lam) accu args | Lprod (dom, codom) -> aux k (aux k accu dom) codom | Llam (ids, body) -> aux (k + Array.length ids) accu body | Llet (_, def, body) -> aux (k + 1) (aux k accu def) body | Lapp (fct, args) -> let accu = aux k accu fct in Array.fold_left (fun accu lam -> aux k accu lam) accu args | Lcase (_, t, a, branches) -> let const = branches.constant_branches in let nonconst = branches.nonconstant_branches in let accu = aux k accu t in let accu = aux k accu a in let accu = Array.fold_left (fun accu lam -> aux k accu lam) accu const in let accu = Array.fold_left (fun accu (ids, lam) -> aux (k + Array.length ids) accu lam) accu nonconst in accu | Lfix (_, (ids, ltypes, lbodies)) | Lcofix (_, (ids, ltypes, lbodies)) -> let accu = Array.fold_left (fun accu lam -> aux k accu lam) accu ltypes in let accu = Array.fold_left (fun accu lam -> aux (k + Array.length ids) accu lam) accu lbodies in accu | Lparray (args, def) -> let accu = Array.fold_left (fun accu lam -> aux k accu lam) accu args in aux k accu def | Lmakeblock (_, _, args) -> Array.fold_left (fun accu lam -> aux k accu lam) accu args | Lprim (_, _, args) -> Array.fold_left (fun accu lam -> aux k accu lam) accu args | Lproj (_, arg) -> aux k accu arg in aux 1 Int.Set.empty lam
(*s Operators on substitution *)let lift = subs_liftlet liftn = subs_liftnlet cons v subst = subs_cons v substlet shift subst = subs_shft (1, subst)
(*s Lift and substitution *)
let rec lam_exlift el lam = match lam.node with | Lrel(id,i) -> let i' = reloc_rel i el in if i == i' then lam else mknode @@ Lrel(id,i') | _ -> map_lam_with_binders el_liftn lam_exlift el lam
let lam_lift k lam = if Int.equal k 0 then lam else lam_exlift (el_shft k el_id) lam
let lam_subst_rel lam id n subst = match expand_rel n subst with | Inl(k,v) -> lam_lift k v | Inr(n',_) -> if n == n' then lam else mknode @@ Lrel(id, n')
let rec lam_exsubst subst lam = match lam.node with | Lrel(id,i) -> lam_subst_rel lam id i subst | _ -> map_lam_with_binders liftn lam_exsubst subst lam
let lam_subst_args subst args = if is_subs_id subst then args else Array.Smart.map (lam_exsubst subst) args
(* [simplify subst lam] simplifies the expression [lam_subst subst lam] by: *)(* - Reducing [let] is the definition can be substituted *)(* - Transforming beta redex into [let] expression *)(* - Moving arguments under [let] *)(* Invariant: Terms in [subst] are already simplified and can be substituted *)
let can_subst lam = match node lam with| Lrel _ | Lvar _ | Lconst _ | Luint _| Lval _ | Lsort _ | Lind _ -> true| Levar _ | Lprod _ | Llam _ | Llet _ | Lapp _ | Lcase _ | Lfix _ | Lcofix _| Lparray _ | Lmakeblock _ | Lfloat _ | Lstring _ | Lprim _ | Lproj _ -> false| Lint _ -> false (* TODO: allow substitution of integers *)
let simplify lam = let rec simplify subst lam = match lam.node with | Lrel(id,i) -> lam_subst_rel lam id i subst
| Llet(id,def,body) -> let def' = simplify subst def in if can_subst def' then simplify (cons def' subst) body else let body' = simplify (lift subst) body in if def == def' && body == body' then lam else mknode @@ Llet(id,def',body')
| Lapp(f,args) -> begin match simplify_app subst f subst args with | { node = Lapp(f',args') } when f == f' && args == args' -> lam | lam' -> lam' end
| _ -> map_lam_with_binders liftn simplify subst lam
and simplify_app substf f substa args = match f.node with | Lrel(id, i) -> begin match lam_subst_rel f id i substf with | { node = Llam(ids, body) } -> reduce_lapp (subs_id 0) (Array.to_list ids) body substa (Array.to_list args) | f' -> mkLapp f' (simplify_args substa args) end | Llam(ids, body) -> reduce_lapp substf (Array.to_list ids) body substa (Array.to_list args) | Llet(id, def, body) -> let def' = simplify substf def in if can_subst def' then simplify_app (cons def' substf) body substa args else mknode @@ Llet(id, def', simplify_app (lift substf) body (shift substa) args) | Lapp(f, args') -> let args = Array.append (lam_subst_args substf args') (lam_subst_args substa args) in simplify_app substf f (subs_id 0) args | _ -> mkLapp (simplify substf f) (simplify_args substa args)
and simplify_args subst args = Array.Smart.map (fun c -> simplify subst c) args
and reduce_lapp substf lids body substa largs = match lids, largs with | id::lids, a::largs -> let a = simplify substa a in if can_subst a then reduce_lapp (subs_cons a substf) lids body substa largs else let body = reduce_lapp (lift substf) lids body (shift substa) largs in mknode @@ Llet(id, a, body) | [], [] -> simplify substf body | _::_, _ -> mknode @@ Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body) | [], _ -> simplify_app substf body substa (Array.of_list largs) in simplify (subs_id 0) lam
(* [occurrence kind k lam]: If [kind] is [true] return [true] if the variable [k] does not appear in [lam], return [false] if the variable appear one time and not under a lambda, a fixpoint, a cofixpoint; else raise Not_found. If [kind] is [false] return [false] if the variable does not appear in [lam] else raise [Not_found]*)
let rec occurrence k kind lam = match lam.node with | Lrel (_,n) -> if n = k then if kind then false else raise Not_found else kind | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ | Lfloat _ | Lstring _ -> kind | Levar (_, args) -> occurrence_args k kind args | Lprod(dom, codom) -> occurrence k (occurrence k kind dom) codom | Llam(ids,body) -> let _ = occurrence (k+Array.length ids) false body in kind | Llet(_,def,body) -> occurrence (k+1) (occurrence k kind def) body | Lapp(f, args) -> occurrence_args k (occurrence k kind f) args | Lparray (args, def) -> occurrence_args k (occurrence k kind def) args | Lprim(_,_,args) | Lmakeblock(_, _,args) -> occurrence_args k kind args | Lcase(_, t, a, branches) -> let kind = occurrence k (occurrence k kind t) a in let r = ref kind in Array.iter (fun c -> r := occurrence k kind c && !r) branches.constant_branches; let on_b (ids,c) = r := occurrence (k+Array.length ids) kind c && !r in Array.iter on_b branches.nonconstant_branches; !r | Lfix(_,(ids,ltypes,lbodies)) | Lcofix(_,(ids,ltypes,lbodies)) -> let kind = occurrence_args k kind ltypes in let _ = occurrence_args (k+Array.length ids) false lbodies in kind | Lproj(_,arg) -> occurrence k kind arg
and occurrence_args k kind args = Array.fold_left (occurrence k) kind args
let occur_once lam = try let _ = occurrence 1 true lam in true with Not_found -> false
(* [remove_let lam] remove let expression in [lam] if the variable is *)(* used at most once time in the body, and does not appear under *)(* a lambda or a fix or a cofix *)
let is_value lam = match node lam with| Lrel _ | Lvar _ | Lconst _ | Luint _| Lval _ | Lsort _ | Lind _ | Lint _ | Llam _ | Lfix _ | Lcofix _ | Lfloat _ | Lstring _ -> true| Levar _ | Lprod _ | Llet _ | Lapp _ | Lcase _| Lparray _ | Lmakeblock _ | Lprim _ | Lproj _ -> false
let rec remove_let subst lam = match lam.node with | Lrel(id,i) -> lam_subst_rel lam id i subst | Llet(id,def,body) -> let def' = remove_let subst def in if is_value body && occur_once body then remove_let (cons def' subst) body else let body' = remove_let (lift subst) body in if def == def' && body == body' then lam else mknode @@ Llet(id,def',body') | _ -> map_lam_with_binders liftn remove_let subst lam
let optimize lam = let lam = simplify lam in let lam = remove_let (subs_id 0) lam in lam
(* Compiling constants *)
let rec get_alias env sigma kn = let cb = CClosure.lookup_constant_handler env sigma.evars_val kn in let tps = cb.const_body_code in match tps with | Vmemitcodes.BCalias kn' -> get_alias env sigma kn' | Vmemitcodes.BCconstant | BCuncompiled -> kn, [||] | Vmemitcodes.BCdefined (mask, _, _) -> kn, mask
(* Translation of constructors *)
let make_args start _end = Array.init (start - _end + 1) (fun i -> mknode @@ Lrel (Anonymous, start - i))
let expand_constructor ind tag nparams arity = let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) let ids = Array.make (nparams + arity) anon in if Int.equal arity 0 then mkLlam ids (mknode @@ (Lint tag)) else let args = make_args arity 1 in mknode @@ Llam(ids, mknode @@ Lmakeblock (ind, tag, args))
let makeblock as_val ind tag nparams arity args = let nargs = Array.length args in if nparams > 0 || nargs < arity then mkLapp (expand_constructor ind tag nparams arity) args else (* The constructor is fully applied *) if arity = 0 then mknode @@ Lint tag else match as_val tag args with | Some v -> mknode @@ Lval v | None -> mknode @@ Lmakeblock (ind, tag, args)
(* Compilation of primitive *)
let prim _env kn p args = mknode @@ Lprim (kn, p, args)
let expand_prim env kn op arity = (* primitives are always Relevant *) let ids = Array.make arity Context.anonR in let args = make_args arity 1 in mknode @@ Llam(ids, prim env kn op args)
let lambda_of_prim env kn op args = let arity = CPrimitives.arity op in match Int.compare (Array.length args) arity with | 0 -> prim env kn op args | x when x > 0 -> let prim_args = Array.sub args 0 arity in let extra_args = Array.sub args arity (Array.length args - arity) in mkLapp(prim env kn op prim_args) extra_args | _ -> mkLapp (expand_prim env kn op arity) args
module RelDecl = Context.Rel.Declaration
type tag = int
module type S =sig type value val as_value : int -> value lambda array -> value option val check_inductive : inductive -> mutual_inductive_body -> unitend
module Make (Val : S) =struct
(* [nparams] is the number of parameters still expected *)let makeblock _env ind tag nparams arity args = makeblock Val.as_value ind tag nparams arity args
(*i Global environment *)
let get_names decl = let decl = Array.of_list decl in Array.map fst decl
let empty_args = [||]
module Cache = struct
module ConstrTable = Hashtbl.Make(Construct.UserOrd)
type constructor_info = tag * int * int (* nparam nrealargs *)
let get_construct_info cache env c : constructor_info = try ConstrTable.find cache c with Not_found -> let ((mind,j), i) = c in let oib = lookup_mind mind env in let oip = oib.mind_packets.(j) in let () = Val.check_inductive (mind, j) oib in let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in let r = (tag, nparams, arity) in ConstrTable.add cache c r; r end
let evar_value sigma ev = sigma.evars_val.CClosure.evar_expand ev
(** Extract the inductive type over which a fixpoint is decreasing *)let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with| Prod (na, dom, t) -> if Int.equal i 0 then let dom = Reduction.whd_all env dom in let (dom, _) = decompose_app dom in match kind dom with | Ind (ind, _) -> ind | _ -> assert false else let env = Environ.push_rel (RelDecl.LocalAssum (na, dom)) env in get_fix_struct env (i - 1) t| _ -> assert false
let rec lambda_of_constr cache env sigma c = match kind c with | Meta _ -> raise (Invalid_argument "lambda_of_constr: Meta")
| Evar ev -> (match evar_value sigma ev with | CClosure.EvarUndefined (evk, args) -> let args = Array.map_of_list (fun c -> lambda_of_constr cache env sigma c) args in mknode @@ Levar(evk, args) | CClosure.EvarDefined t -> lambda_of_constr cache env sigma t)
| Cast (c, _, _) -> lambda_of_constr cache env sigma c
| Rel i -> mknode @@ Lrel (RelDecl.get_name (Environ.lookup_rel i env), i)
| Var id -> mknode @@ Lvar id
| Sort s -> mknode @@ Lsort s
| Ind pind -> mknode @@ Lind pind
| Prod(id, dom, codom) -> let ld = lambda_of_constr cache env sigma dom in let env = Environ.push_rel (RelDecl.LocalAssum (id, dom)) env in let lc = lambda_of_constr cache env sigma codom in mknode @@ Lprod(ld, mknode @@ Llam([|id|], lc))
| Lambda _ -> let params, body = Term.decompose_lambda c in let fold (na, t) env = Environ.push_rel (RelDecl.LocalAssum (na, t)) env in let env = List.fold_right fold params env in let lb = lambda_of_constr cache env sigma body in let ids = get_names (List.rev params) in mkLlam ids lb
| LetIn(id, def, t, body) -> let ld = lambda_of_constr cache env sigma def in let env = Environ.push_rel (RelDecl.LocalDef (id, def, t)) env in let lb = lambda_of_constr cache env sigma body in mknode @@ Llet(id, ld, lb)
| App(f, args) -> lambda_of_app cache env sigma f args
| Const _ -> lambda_of_app cache env sigma c empty_args
| Construct _ -> lambda_of_app cache env sigma c empty_args
| Proj (p, _, c) -> let c = lambda_of_constr cache env sigma c in mknode @@ Lproj (Projection.repr p, c)
| Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *) let (ci, (t,_), _iv, a, branches) = Inductive.expand_case env (ci, u, pms, t, iv, a, br) in let (mind, i) = ci.ci_ind in let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in let tbl = oib.mind_reloc_tbl in (* Building info *) let annot_sw = (ci, tbl, mib.mind_finite) in (* translation of the argument *) let la = lambda_of_constr cache env sigma a in (* translation of the type *) let lt = lambda_of_constr cache env sigma t in (* translation of branches *) let dummy = mknode @@ Lrel(Anonymous,0) in let consts = Array.make oib.mind_nb_constant dummy in let blocks = Array.make oib.mind_nb_args ([||],dummy) in let rtbl = oib.mind_reloc_tbl in for i = 0 to Array.length rtbl - 1 do let tag, arity = rtbl.(i) in let b = lambda_of_constr cache env sigma branches.(i) in if arity = 0 then consts.(tag) <- b else let b = match b.node with | Llam (ids, body) when arity <= Array.length ids -> let ids, rem = Array.chop arity ids in (ids, mkLlam rem body) | _ -> (* happens when the branch contains let-bindings *) let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) let ids = Array.make arity anon in let args = make_args arity 1 in let ll = lam_lift arity b in (ids, mkLapp ll args) in blocks.(tag-1) <- b done; let branches = { constant_branches = consts; nonconstant_branches = blocks } in mknode @@ Lcase(annot_sw, lt, la, branches)
| Fix((pos, i), (names,type_bodies,rec_bodies)) -> let ltypes = lambda_of_args cache env sigma 0 type_bodies in let map i t = get_fix_struct env i t in let inds = Array.map2 map pos type_bodies in let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in let lbodies = lambda_of_args cache env sigma 0 rec_bodies in mknode @@ Lfix((pos, inds, i), (names, ltypes, lbodies))
| CoFix(init,(names,type_bodies,rec_bodies)) -> let ltypes = lambda_of_args cache env sigma 0 type_bodies in let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in let map c ty = Reduction.eta_expand env c (Vars.lift (Array.length type_bodies) ty) in let rec_bodies = Array.map2 map rec_bodies type_bodies in let lbodies = lambda_of_args cache env sigma 0 rec_bodies in mknode @@ Lcofix(init, (names, ltypes, lbodies))
| Int i -> mknode @@ Luint i
| Float f -> mknode @@ Lfloat f
| String s -> mknode @@ (Lstring s)
| Array (_u, t, def, _ty) -> let def = lambda_of_constr cache env sigma def in mknode @@ Lparray (lambda_of_args cache env sigma 0 t, def)
and lambda_of_app cache env sigma f args = match kind f with | Const (kn, u as c) -> let kn, mask = get_alias env sigma kn in let cb = CClosure.lookup_constant_handler env sigma.evars_val kn in begin match cb.const_body with | Primitive op -> lambda_of_prim env c op (lambda_of_args cache env sigma 0 args) | Def csubst -> (* TODO optimize if f is a proj and argument is known *) if cb.const_inline_code then let csubst = Vars.subst_instance_constr u csubst in lambda_of_app cache env sigma csubst args else (* Erase unused arguments *) let mapi i arg = let keep = if i < Array.length mask then mask.(i) else true in if keep then lambda_of_constr cache env sigma arg else mknode (Lint 0) (* dummy *) in let args = Array.mapi mapi args in mkLapp (mknode @@ Lconst (kn, u)) args | OpaqueDef _ | Undef _ | Symbol _ -> mkLapp (mknode @@ Lconst (kn, u)) (lambda_of_args cache env sigma 0 args) end | Construct ((ind,_ as c),_) -> let tag, nparams, arity = Cache.get_construct_info cache env c in let nargs = Array.length args in if nparams < nargs then (* got all parameters *) let args = lambda_of_args cache env sigma nparams args in makeblock env ind tag 0 arity args else makeblock env ind tag (nparams - nargs) arity empty_args | _ -> let f = lambda_of_constr cache env sigma f in let args = lambda_of_args cache env sigma 0 args in mkLapp f args
and lambda_of_args cache env sigma start args = let nargs = Array.length args in if start < nargs then Array.init (nargs - start) (fun i -> lambda_of_constr cache env sigma args.(start + i)) else empty_args
let lambda_of_constr env sigma c = let cache = Cache.ConstrTable.create 91 in lambda_of_constr cache env sigma c
end