Stefan pushed to branch master at Stefan / Typer

Commits: 4a267fe6 by Stefan Monnier at 2018-05-03T20:03:37Z * src/opslexp.ml (mktup, ctx2tup): New functions

- - - - -

1 changed file:

- src/opslexp.ml

Changes:

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps

-Copyright (C) 2011-2017 Free Software Foundation, Inc. +Copyright (C) 2011-2018 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -31,6 +31,7 @@ module P = Pexp open Lexp module E = Elexp module L = Lexp +module M = Myers

(* open Unify *) module S = Subst @@ -923,4 +924,42 @@ and clean_map cases = -> (l, (clean_arg_list args), (erase_type expr))) cases

+(** Turning a set of declarations into an object. **) + +let mktup types vals = + let loc = DB.dloc in + let cons_name = "cons" in + let cons_label = (loc, cons_name) in + let type_label = (loc, "record") in + Call (Cons (Inductive (loc, type_label, [], + SMap.add cons_name + (List.map (fun (oname, t) + -> (P.Aimplicit, oname, t)) + types) + SMap.empty), + cons_label), + List.map (fun v -> (P.Aimplicit, v)) vals) + +let ctx2tup ctx nctx = + assert (M.length nctx >= M.length ctx + && ctx == M.nthcdr (M.length nctx - M.length ctx) nctx); + let rec get_ts_vs nctx types vals = + if nctx == ctx then (types, vals) else + match DB.lctx_view nctx with + | DB.CVlet (oname, LetDef e, t, nctx) + -> get_ts_vs nctx ((oname, t) :: types) (e :: vals) + | DB.CVfix (defs, nctx) + -> let rec shift_vs rdefs types vals defs = match rdefs with + | [] -> get_ts_vs nctx types vals + | (oname, LetDef e, t) :: rdefs + -> let name = maybev oname in + let defs = (name, e, t) :: defs in + shift_vs rdefs ((oname, t) :: types) + (Let (DB.dloc, defs, e) :: vals) defs + | _ -> U.internal_error "ctx2tup: Non-letdef in recursive vars" in + shift_vs (List.rev defs) types vals [] + | _ -> assert false in + let (types, vals) = get_ts_vs nctx [] [] in + mktup types vals + (* opslexp.ml ends here. *)

View it on GitLab: https://gitlab.com/monnier/typer/commit/4a267fe6d6392402546d4a988f5448bc5157...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/4a267fe6d6392402546d4a988f5448bc5157... You're receiving this email because of your account on gitlab.com.