Skip to content

GitLab

Commit 08f6b841 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2002-11-10 16:13:31 by cvscast] Empty log message 

Original author: cvscast
Date: 2002-11-10 16:13:32+00:00
parent 7b6fcfba
Hide whitespace changes
Inline Side-by-side
depend
View file @ 08f6b841
......@@ -22,12 +22,10 @@ typing/typed.cmx: parser/location.cmx types/patterns.cmx types/sortedMap.cmx \
types/types.cmx
typing/typer.cmo: parser/ast.cmo types/builtin.cmo types/intervals.cmi \
parser/location.cmi types/patterns.cmi types/sequence.cmi \
types/sortedList.cmi misc/state.cmi typing/typed.cmo types/types.cmi \
typing/typer.cmi
types/sortedList.cmi typing/typed.cmo types/types.cmi typing/typer.cmi
typing/typer.cmx: parser/ast.cmx types/builtin.cmx types/intervals.cmx \
parser/location.cmx types/patterns.cmx types/sequence.cmx \
types/sortedList.cmx misc/state.cmx typing/typed.cmx types/types.cmx \
typing/typer.cmi
types/sortedList.cmx typing/typed.cmx types/types.cmx typing/typer.cmi
types/atoms.cmo: types/sortedList.cmi types/atoms.cmi
types/atoms.cmx: types/sortedList.cmx types/atoms.cmi
types/boolean.cmo: types/recursive.cmo types/sortedList.cmi types/boolean.cmi
......@@ -96,10 +94,10 @@ driver/cduce.cmx: parser/ast.cmx types/builtin.cmx runtime/eval.cmx \
parser/wlexer.cmx driver/cduce.cmi
driver/run.cmo: driver/cduce.cmi parser/location.cmi misc/state.cmi
driver/run.cmx: driver/cduce.cmx parser/location.cmx misc/state.cmx
driver/webiface.cmo: driver/cduce.cmi runtime/load_xml.cmi \
parser/location.cmi
driver/webiface.cmx: driver/cduce.cmx runtime/load_xml.cmx \
parser/location.cmx
driver/webiface.cmo: driver/cduce.cmi runtime/eval.cmi runtime/load_xml.cmi \
parser/location.cmi misc/state.cmi
driver/webiface.cmx: driver/cduce.cmx runtime/eval.cmx runtime/load_xml.cmx \
parser/location.cmx misc/state.cmx
parser/parser.cmi: parser/ast.cmo
typing/typer.cmi: parser/ast.cmo typing/typed.cmo types/types.cmi
types/boolean.cmi: types/sortedList.cmi
......@@ -113,3 +111,4 @@ runtime/eval.cmi: typing/typed.cmo runtime/value.cmi
runtime/load_xml.cmi: runtime/value.cmi
runtime/run_dispatch.cmi: types/patterns.cmi runtime/value.cmi
runtime/value.cmi: types/chars.cmi types/sortedMap.cmi types/types.cmi
driver/cduce.cmi: runtime/eval.cmi typing/typer.cmi
driver/cduce.ml
View file @ 08f6b841
open Location
let typing_env = State.ref "Cduce.typing_env" Typer.Env.empty
let glb_env = State.ref "Cduce.glb_env" Typer.Env.empty
let eval_env = Eval.global_env
let print_norm ppf d =
Location.protect ppf
(fun ppf -> Types.Print.print_descr ppf ((*Types.normalize*) d))
......@@ -7,6 +11,21 @@ let print_norm ppf d =
let print_value ppf v =
Location.protect ppf (fun ppf -> Value.print ppf v)
let dump_env ppf =
Format.fprintf ppf "Global types:";
Typer.Env.iter (fun x _ -> Format.fprintf ppf " %s" x) !glb_env;
Format.fprintf ppf ".@\n";
Eval.Env.iter
(fun x v ->
let t = Typer.Env.find x !typing_env in
Format.fprintf ppf "@[|- %s : %a@ => %a@]@\n"
x
print_norm t
print_value v
)
!eval_env
let rec print_exn ppf = function
| Location (loc, exn) ->
Format.fprintf ppf "Error %a:@\n" Location.print_loc loc;
......@@ -61,28 +80,28 @@ let rec print_exn ppf = function
let debug ppf = function
| `Filter (t,p) ->
Format.fprintf ppf "[DEBUG:filter]@\n";
let t = Typer.typ t
and p = Typer.pat p in
let t = Typer.typ !glb_env t
and p = Typer.pat !glb_env p in
let f = Patterns.filter (Types.descr t) p in
List.iter (fun (x,t) ->
Format.fprintf ppf " %s:%a@\n" x
print_norm (Types.descr t)) f
| `Accept p ->
Format.fprintf ppf "[DEBUG:accept]@\n";
let p = Typer.pat p in
let p = Typer.pat !glb_env p in
let t = Patterns.accept p in
Format.fprintf ppf " %a@\n" Types.Print.print t
| `Compile (t,pl) ->
Format.fprintf ppf "[DEBUG:compile]@\n";
let t = Typer.typ t
and pl = List.map Typer.pat pl in
let t = Typer.typ !glb_env t
and pl = List.map (Typer.pat !glb_env) pl in
let pl = Array.of_list
(List.map (fun p -> Patterns.Compile.normal
(Patterns.descr p)) pl) in
Patterns.Compile.show ppf (Types.descr t) pl
| `Normal_record t ->
Format.fprintf ppf "[DEBUG:normal_record]@\n";
let t = Types.descr (Typer.typ t) in
let t = Types.descr (Typer.typ !glb_env t) in
let count = ref 0 and seen = ref [] in
match Types.Record.first_label t with
| `Empty -> Format.fprintf ppf "Empty"
......@@ -101,7 +120,7 @@ let debug ppf = function
(*
| `Normal_record t ->
Format.fprintf ppf "[DEBUG:normal_record]@\n";
let t = Types.descr (Typer.typ t) in
let t = Types.descr (Typer.typ !glb_env t) in
let r = Types.Record.normal t in
let count = ref 0 and seen = ref [] in
let rec aux ppf x =
......@@ -128,15 +147,14 @@ let debug ppf = function
*)
let mk_builtin () =
List.iter
(fun (n,t) -> Typer.register_global_types [n, mk noloc (Ast.Internal t)])
Builtin.types
let bi = List.map (fun (n,t) -> [n, mk noloc (Ast.Internal t)])
Builtin.types in
glb_env := List.fold_left Typer.register_global_types !glb_env bi
let () = mk_builtin ()
let typing_env = State.ref "Cduce.typing_env" Typer.Env.empty
let eval_env = State.ref "Cduce.eval_env" Eval.Env.empty
let run ppf input =
let insert_type_bindings =
......@@ -150,7 +168,7 @@ let run ppf input =
in
let eval_decl decl =
let bindings = Eval.eval_let_decl !eval_env decl in
let bindings = Eval.eval_let_decl Eval.Env.empty decl in
List.iter
(fun (x,v) ->
Eval.enter_global x v;
......@@ -161,15 +179,15 @@ let run ppf input =
let phrase ph =
match ph.descr with
| Ast.EvalStatement e ->
let (fv,e) = Typer.expr e in
let (fv,e) = Typer.expr !glb_env e in
let t = Typer.type_check !typing_env e Types.any true in
Location.dump_loc ppf e.Typed.exp_loc;
Format.fprintf ppf "|- %a@\n@." print_norm t;
let v = Eval.eval !eval_env e in
let v = Eval.eval Eval.Env.empty e in
Format.fprintf ppf "=> @[%a@]@\n@." print_value v
| Ast.LetDecl (p,{descr=Ast.Abstraction _}) -> ()
| Ast.LetDecl (p,e) ->
let decl = Typer.let_decl p e in
let decl = Typer.let_decl !glb_env p e in
type_decl decl;
eval_decl decl
| Ast.TypeDecl _ -> ()
......@@ -178,7 +196,7 @@ let run ppf input =
in
let do_fun_decls decls =
let decls = List.map (fun (p,e) -> Typer.let_decl p e) decls in
let decls = List.map (fun (p,e) -> Typer.let_decl !glb_env p e) decls in
insert_type_bindings (Typer.type_rec_funs !typing_env decls);
List.iter eval_decl decls
in
......@@ -197,7 +215,7 @@ let run ppf input =
(typs, (p,e)::funs)
| _ -> accu
) ([],[]) p in
Typer.register_global_types type_decls;
glb_env := Typer.register_global_types !glb_env type_decls;
do_fun_decls fun_decls;
List.iter phrase p;
true
......
driver/cduce.mli
View file @ 08f6b841
val typing_env: Typer.env ref (* Types of toplevel bindings *)
val eval_env: Eval.env ref (* Values of toplevel bindings *)
val glb_env: Typer.glb ref (* Global types *)
val print_exn: Format.formatter -> exn -> unit
val run : Format.formatter -> char Stream.t -> bool
(* Returns true if everything is ok (no error) *)
val dump_env : Format.formatter -> unit
driver/webiface.ml
View file @ 08f6b841
......@@ -139,15 +139,9 @@ let main (cgi : Netcgi.std_activation) =
if !persistant then check_session_id !session_id;
let dialog content = html_form p content in
let exec src =
let ppf = Format.str_formatter
and input = Stream.of_string src in
Location.set_source (`String src);
Location.set_viewport `Html;
Load_xml.set_auth false;
if !persistant then (
let load_state () =
if !persistant then
try
let chan = open_in_bin (session_file !session_id) in
if in_channel_length chan > 0 then
......@@ -156,29 +150,51 @@ let main (cgi : Netcgi.std_activation) =
close_in chan;
with Sys_error _ ->
failwith "This session has expired ..."
);
in
let store_state () =
if !persistant then
let s = State.get () in
let chan = open_out_bin (session_file !session_id) in
Marshal.to_channel chan s [ Marshal.Closures ];
close_out chan
in
let exec src =
let ppf = Format.str_formatter
and input = Stream.of_string src in
Location.set_source (`String src);
Load_xml.set_auth false;
load_state ();
let ok = Cduce.run ppf input in
if ok then Format.fprintf ppf "@\nOk.@\n";
let res = Format.flush_str_formatter () in
cgi # output # output_string ("<pre>" ^ res ^ "</pre>");
if ok then dialog "" else dialog src;
if ok then (dialog ""; store_state ()) else dialog src;
in
if ok && !persistant then (
let s = State.get () in
let chan = open_out_bin (session_file !session_id) in
Marshal.to_channel chan s [ Marshal.Closures ];
close_out chan
)
let dump src =
let ppf = Format.str_formatter in
load_state ();
store_state (); (* Just touch the file ... *)
Format.fprintf ppf "<b>Environment</b>:@.";
Cduce.dump_env ppf;
let res = Format.flush_str_formatter () in
cgi # output # output_string ("<pre>" ^ res ^ "</pre>");
dialog src
in
Location.set_viewport `Html;
html_header p;
let prog = cgi # argument_value "prog" in
(match cmd with
| `Exec -> exec prog
| `Open -> dialog prog
| `New -> dialog ""
| `Dump -> failwith "Dump not yet implemented"
| `Dump -> dump prog
| `Close -> dialog ""
);
html_footer p;
......
parser/ast.ml
View file @ 08f6b841
......@@ -22,9 +22,6 @@ and debug_directive =
and pexpr = pexpr' located
and pexpr' =
(* For debugging the typer: an expression with prescribed type *)
| DebugTyper of ppat
| Forget of pexpr * ppat
(* CDuce is a Lambda-calculus ... *)
| Var of string
......
parser/location.ml
View file @ 08f6b841
......@@ -5,6 +5,9 @@ type viewport = [ `Html | `Text ]
exception Location of loc * exn
exception Generic of string
let raise_generic s = raise (Generic s)
let raise_loc_generic loc s = raise (Location (loc, Generic s))
let noloc = (-1,-1)
let source = ref `None
......@@ -57,14 +60,19 @@ let dump_loc ppf (i,j) =
| _ -> ()
let rec beg_of_line s i =
if (i = 0) || (s.[i-1] = '\n') then i else beg_of_line s (i - 1)
if (i = 0) || (s.[i-1] = '\n') || (s.[i-1] = '\r')
then i else beg_of_line s (i - 1)
let rec end_of_line s i =
if (i = String.length s) || (s.[i] = '\n') then i else end_of_line s (i + 1)
if (i = String.length s) || (s.[i] = '\n') || (s.[i] = '\r')
then i else end_of_line s (i + 1)
let html_hilight ppf (i,j) =
match (!source, !viewport) with
| `String s, `Html ->
if (i < 0) then
Format.fprintf ppf "<b>GHOST LOCATION</b>@\n"
else
let i0 = beg_of_line s i in
let j0 = end_of_line s j in
Format.fprintf ppf
......
parser/location.mli
View file @ 08f6b841
......@@ -6,6 +6,9 @@ exception Location of loc * exn
exception Generic of string
val noloc:loc
val raise_generic: string -> 'a
val raise_loc_generic: loc -> string -> 'a
type source = [ `None | `File of string | `Stream | `String of string ]
val set_source: source -> unit
......
runtime/eval.ml
View file @ 08f6b841
......@@ -63,7 +63,6 @@ let rec eval env e0 =
| Typed.Op ("print_xml", [e]) -> eval_print_xml (eval env e)
| Typed.Op ("int_of", [e]) -> eval_int_of (eval env e)
| Typed.Dot (e, l) -> eval_dot l (eval env e)
| Typed.DebugTyper t -> failwith "Evaluating a ! expression"
| Typed.Op (o,_) -> failwith ("Unknown operator " ^ o)
......
runtime/eval.mli
View file @ 08f6b841
......@@ -3,6 +3,7 @@ open Value
module Env : Map.S with type key = string
type env = t Env.t
val global_env : env ref
val enter_global : string -> t -> unit
......
types/patterns.ml
View file @ 08f6b841
......@@ -7,8 +7,8 @@
type capture = string
type fv = capture SortedList.t
exception IllFormedCup of fv * fv
exception IllFormedCap of fv * fv
exception Error of string
(* Syntactic algebra *)
......@@ -40,10 +40,27 @@ let define x ((accept,fv,_) as d) =
let constr x = (Types.descr x,[],Constr x)
let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) =
if fv1 <> fv2 then raise (IllFormedCup (fv1,fv2));
if fv1 <> fv2 then (
let x = match SortedList.diff fv1 fv2 with
| x::_ -> x
| [] -> match SortedList.diff fv2 fv1 with x::_ -> x | _ -> assert false
in
raise
(Error
("The capture variable " ^ x ^
" should appear on both side of this | pattern"))
);
(Types.cup acc1 acc2, SortedList.cup fv1 fv2, Cup (x1,x2))
let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) e =
if not (SortedList.disjoint fv1 fv2) then raise (IllFormedCap (fv1,fv2));
if not (SortedList.disjoint fv1 fv2) then (
match SortedList.cap fv1 fv2 with
| x::_ ->
raise
(Error
("The capture variable " ^ x ^
" cannot appear on both side of this & pattern"))
| _ -> assert false
);
(Types.cap acc1 acc2, SortedList.cup fv1 fv2, Cap (x1,x2,e))
let times x y =
(Types.times x.accept y.accept, SortedList.cup x.fv y.fv, Times (x,y))
......
types/patterns.mli
View file @ 08f6b841
type capture = string
type fv = capture SortedList.t
exception IllFormedCup of fv * fv
exception IllFormedCap of fv * fv
exception Error of string
(* Pattern algebra *)
......
typing/typed.ml
View file @ 08f6b841
......@@ -19,8 +19,6 @@ type texpr = { exp_loc : loc;
exp_descr : texpr';
}
and texpr' =
| DebugTyper of ttyp
| Forget of texpr * ttyp
(* CDuce is a Lambda-calculus ... *)
| Var of string
......
typing/typer.ml
View file @ 08f6b841
......@@ -4,7 +4,6 @@
open Location
open Ast
exception Pattern of string
exception NonExhaustive of Types.descr
exception MultipleLabel of Types.label
exception Constraint of Types.descr * Types.descr * string
......@@ -44,6 +43,8 @@ module S = struct type t = string let compare = compare end
module StringMap = Map.Make(S)
module StringSet = Set.Make(S)
type glb = ti StringMap.t
let mk' =
let counter = ref 0 in
fun loc ->
......@@ -96,6 +97,8 @@ module Regexp = struct
| `Star of flat
| `WeakStar of flat ]
let re_loc = ref noloc
let rec propagate vars : regexp -> flat = function
| Epsilon -> `Epsilon
| Elem x -> let p = vars x in `Elem (uniq_id (),p)
......@@ -104,14 +107,14 @@ module Regexp = struct
| Star r -> `Star (propagate vars r)
| WeakStar r -> `WeakStar (propagate vars r)
| SeqCapture (v,x) ->
let v= mk noloc (Capture v) in
propagate (fun p -> mk noloc (And (vars p,v,true))) x
let v= mk !re_loc (Capture v) in
propagate (fun p -> mk !re_loc (And (vars p,v,true))) x
let cup r1 r2 =
match (r1,r2) with
| (_, `Empty) -> r1
| (`Empty, _) -> r2
| (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))
| (`Res t1, `Res t2) -> `Res (mk !re_loc (Or (t1,t2)))
(*TODO: review this compilation schema to avoid explosion when
coding (Optional x) by (Or(Epsilon,x)); memoization ... *)
......@@ -130,7 +133,7 @@ module Regexp = struct
| `Epsilon :: rest ->
compile fin e rest
| `Elem (_,p) :: rest ->
`Res (mk noloc (Prod (p, guard_compile fin rest)))
`Res (mk !re_loc (Prod (p, guard_compile fin rest)))
| `Seq (r1,r2) :: rest ->
compile fin e (r1 :: r2 :: rest)
| `Alt (r1,r2) :: rest ->
......@@ -145,7 +148,7 @@ module Regexp = struct
with
Not_found ->
let n = name () in
let v = mk noloc (PatVar n) in
let v = mk !re_loc (PatVar n) in
memo := Memo.add seq v !memo;
let d = compile fin (ref Coind.empty) seq in
(match d with
......@@ -155,19 +158,22 @@ module Regexp = struct
let constant_nil v t =
mk noloc (And (t, (mk noloc (Constant (v, Types.Atom Sequence.nil_atom))), true))
mk !re_loc
(And (t,
(mk !re_loc (Constant (v, Types.Atom Sequence.nil_atom))), true))
let compile regexp queue : ppat =
let compile loc regexp queue : ppat =
re_loc := loc;
let vars = seq_vars StringSet.empty regexp in
let fin = StringSet.fold constant_nil vars queue in
let fin = StringSet.fold constant_nil vars queue in
let n = guard_compile fin [propagate (fun p -> p) regexp] in
memo := Memo.empty;
let d = !defs in
defs := [];
mk noloc (Recurs (n,d))
mk !re_loc (Recurs (n,d))
end
let compile_regexp = Regexp.compile
let compile_regexp = Regexp.compile noloc
let rec compile env { loc = loc; descr = d } : ti =
......@@ -175,10 +181,10 @@ let rec compile env { loc = loc; descr = d } : ti =
| PatVar s ->
(try StringMap.find s env
with Not_found ->
raise_loc loc (Pattern ("Undefined type variable " ^ s))
raise_loc_generic loc ("Undefined type variable " ^ s)
)
| Recurs (t, b) -> compile (compile_many env b) t
| Regexp (r,q) -> compile env (Regexp.compile r q)
| Regexp (r,q) -> compile env (Regexp.compile loc r q)
| Internal t -> cons loc (`Type t)
| Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
| And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e))
......@@ -196,7 +202,6 @@ and compile_many env b =
List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;
env
let comp_fv_seen = ref []
let comp_fv_res = ref []
let rec comp_fv s =
......@@ -235,9 +240,8 @@ let rec typ seen s : Types.descr =
match s.descr' with
| `Alias (v,x) ->
if List.memq s seen then
raise_loc s.loc'
(Pattern
("Unguarded recursion on variable " ^ v ^ " in this type"))
raise_loc_generic s.loc'
("Unguarded recursion on variable " ^ v ^ " in this type")
else typ (s :: seen) x
| `Type t -> t
| `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
......@@ -266,30 +270,34 @@ let type_node s =
let rec pat seen s : Patterns.descr =
if fv s = [] then Patterns.constr (type_node s) else
match s.descr' with
| `Alias (v,x) ->
if List.memq s seen then
raise_loc s.loc'
(Pattern
("Unguarded recursion on variable " ^ v ^ " in this pattern"))
else pat (s :: seen) x
| `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
| `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e
| `Diff (s1,s2) when fv s2 = [] ->
let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
Patterns.cap (pat seen s1) (Patterns.constr s2) true
| `Diff _ ->
raise_loc s.loc' (Pattern "Difference not allowed in patterns")
| `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
| `Record (l,false,s) -> Patterns.record l (pat_node s)
| `Record _ ->
raise_loc s.loc'
(Pattern "Optional field not allowed in record patterns")
| `Capture x -> Patterns.capture x
| `Constant (x,c) -> Patterns.constant x c
| `Arrow _ ->
raise_loc s.loc' (Pattern "Arrow not allowed in patterns")
| `Type _ -> assert false
try pat_aux seen s
with Patterns.Error e -> raise_loc_generic s.loc' e
| Location (loc,exn) when loc = noloc -> raise (Location (s.loc', exn))
and pat_aux seen s = match s.descr' with
| `Alias (v,x) ->
if List.memq s seen
then raise
(Patterns.Error
("Unguarded recursion on variable " ^ v ^ " in this pattern"));
pat (s :: seen) x
| `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
| `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e
| `Diff (s1,s2) when fv s2 = [] ->
let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
Patterns.cap (pat seen s1) (Patterns.constr s2) true
| `Diff _ ->
raise (Patterns.Error "Difference not allowed in patterns")
| `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
| `Record (l,false,s) -> Patterns.record l (pat_node s)
| `Record _ ->
raise (Patterns.Error "Optional field not allowed in record patterns")
| `Capture x -> Patterns.capture x
| `Constant (x,c) -> Patterns.constant x c
| `Arrow _ ->
raise (Patterns.Error "Arrow not allowed in patterns")
| `Type _ -> assert false
and pat_node s : Patterns.node =
match s.pat_node with
......@@ -301,59 +309,56 @@ and pat_node s : Patterns.node =
Patterns.define x t;
x
let global_types = State.ref "Typer.global_types" StringMap.empty
let mk_typ e =
if fv e = [] then type_node e
else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")
else raise_loc_generic e.loc' "Capture variables are not allowed in types"
let typ e =
mk_typ (compile !global_types e)
let typ glb e =
mk_typ (compile glb e)
let pat glb e =
pat_node (compile glb e)
let pat e =
let e = compile !global_types e in
pat_node e
let register_global_types glb b =
let env' = compile_many glb b in
List.fold_left
(fun glb (v,{ loc = loc }) ->
let t = StringMap.find v env' in
let d = Types.descr (mk_typ t) in
(* let d = Types.normalize d in*)
Types.Print.register_global v d;
if StringMap.mem v glb
</