Stefan pushed to branch master at Stefan / Typer
Commits:
d6005a0c by Stefan Monnier at 2018-05-18T17:44:46Z
* src/lexp.ml (push_susp): Fix list inversion
Reported by Jonathan Graveline.
- - - - -
1 changed file:
- src/lexp.ml
Changes:
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -272,11 +272,11 @@ let rec push_susp e s = (* Push a suspension one level down. *)
| Let (l, defs, e)
-> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in
- let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty)
- -> (ssink v s,
- (v, mkSusp def s', mkSusp ty s) :: ndefs))
- (s, []) defs in
- mkLet (l, ndefs, mkSusp e s')
+ let rec loop s defs = match defs with
+ | [] -> []
+ | (v, def, ty) :: defs
+ -> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in
+ mkLet (l, loop s defs, mkSusp e s')
| Arrow (ak, v, t1, l, t2)
-> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s))
| Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s))
View it on GitLab: https://gitlab.com/monnier/typer/commit/d6005a0ccdd2ff8735c831ee989da65891e…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/d6005a0ccdd2ff8735c831ee989da65891e…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
bfa8bdcf by Jonathan Graveline at 2018-05-17T22:16:53Z
Change from master
- - - - -
1 changed file:
- src/util.ml
Changes:
=====================================
src/util.ml
=====================================
--- a/src/util.ml
+++ b/src/util.ml
@@ -86,7 +86,7 @@ let msg_info = msg_message 3 "Info:"
(* Compiler Internal Debug print *)
let debug_msg expr =
- if 4 <= !_typer_verbose then expr else ()
+ if 4 <= !_typer_verbose then (print_string expr; flush stdout) else ()
let not_implemented_error () = internal_error "not implemented"
View it on GitLab: https://gitlab.com/monnier/typer/commit/bfa8bdcf9abaf63f2952fcf1e252878789e…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/bfa8bdcf9abaf63f2952fcf1e252878789e…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
3da1ce59 by Jonathan Graveline at 2018-05-17T22:15:49Z
push_susp reverse let definition (not sure if it was an error)
- - - - -
1 changed file:
- src/lexp.ml
Changes:
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -276,7 +276,9 @@ let rec push_susp e s = (* Push a suspension one level down. *)
-> (ssink v s,
(v, mkSusp def s', mkSusp ty s) :: ndefs))
(s, []) defs in
- mkLet (l, ndefs, mkSusp e s')
+ (* Why does definition list was reversed? It do not break anything to reverse it back! *)
+ (*mkLet (l, ndefs, mkSusp e s')*)
+ mkLet (l, List.rev ndefs, mkSusp e s')
| Arrow (ak, v, t1, l, t2)
-> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink (maybev v) s))
| Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s))
View it on GitLab: https://gitlab.com/monnier/typer/commit/3da1ce59a158f3f579cb312d1d7e303baa7…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/3da1ce59a158f3f579cb312d1d7e303baa7…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
bd6a3933 by Jonathan Graveline at 2018-05-17T22:09:07Z
Replace elab.ml
- - - - -
1 changed file:
- src/elab.ml
Changes:
=====================================
src/elab.ml
=====================================
--- a/src/elab.ml
+++ b/src/elab.ml
@@ -1548,7 +1548,7 @@ let sform_load usr_elctx loc sargs ot =
(* create a tuple from context and shift it to user context *)
let tuple = OL.ctx2tup dflt_lctx ld_lctx in
- let tuple' = Lexp.mkSusp tuple (S.shift (usr_len - dflt_len)) in
+ let tuple' = (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in
(tuple',Lazy)
View it on GitLab: https://gitlab.com/monnier/typer/commit/bd6a3933c6a3a9c12e6a7f4130700476781…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/bd6a3933c6a3a9c12e6a7f4130700476781…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
3d4d9623 by Jonathan Graveline at 2018-05-17T00:33:20Z
Unfinished work on ctx2tup and mktup
- - - - -
1 changed file:
- src/opslexp.ml
Changes:
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -925,6 +925,8 @@ and clean_map cases =
cases
(** Turning a set of declarations into an object. **)
+
+let shift n lexp = Lexp.mkSusp lexp (S.shift n)
let mktup types vals =
let loc = DB.dloc in
@@ -932,37 +934,50 @@ let mktup types vals =
let cons_label = (loc, cons_name) in
let type_label = (loc, "record") in
- let shift n lexp = Lexp.mkSusp lexp (S.Shift (S.Identity,n)) in
+ let self_len = List.length types in
+
+ let nlet l (oname,t) e = Let (DB.dloc, [((maybev oname), e, t)], l) in
+ (*let nlet l (oname,t) e = ((maybev oname), shift (self_len - (List.length l)) e, t) :: l in*)
- Call (Cons (Inductive (loc, type_label, [],
+ let body = Call (Cons (Inductive (loc, type_label, [],
SMap.add cons_name
(List.map (fun (oname, t)
- -> (P.Aimplicit, oname, t))
+ -> (P.Aimplicit, oname, shift self_len t))
types)
SMap.empty),
cons_label),
- (* shift could be done in sform_load but it is easy to put it here *)
- List.mapi (fun n v -> (P.Aimplicit, shift (- n) v)) vals)
+
+ List.mapi (fun n v -> (
+ (P.Aimplicit, shift (self_len - n - 1) v)
+
+ ))
+ vals
+ ) in
+
+ List.fold_left2 nlet body (List.rev types) (List.rev vals)
+ (*Let (DB.dloc, List.rev (List.fold_left2 nlet [] types vals), body)*)
-(* does not seem to let previous global declaration be used by next global declaration *)
let ctx2tup ctx nctx =
assert (M.length nctx >= M.length ctx
&& ctx == M.nthcdr (M.length nctx - M.length ctx) nctx);
+
+ let to_rdef l rdef = match rdef with
+ | (oname, LetDef e, t) -> (oname, t) :: l
+ | _ -> U.internal_error "ctx2tup: Non-letdef in recursive vars" in
+
+ let to_rval l rdef = match rdef with
+ | (oname, LetDef e, t) -> e :: l
+ | _ -> U.internal_error "ctx2tup: Non-letdef in recursive vars" in
+
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 []
+ -> let rtypes = (List.fold_left to_rdef [] defs) in
+ let rvals = (List.fold_left to_rval [] defs) in
+ get_ts_vs nctx (List.concat (rtypes :: [types])) (List.concat (rvals :: [vals]))
| _ -> assert false in
let (types, vals) = get_ts_vs nctx [] [] in
mktup types vals
View it on GitLab: https://gitlab.com/monnier/typer/commit/3d4d9623830585cfbafa147a42cc8187235…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/3d4d9623830585cfbafa147a42cc8187235…
You're receiving this email because of your account on gitlab.com.